modernized proofs with bullets

Author: palmskog

classical.v

@@ -11,22 +11,22 @@ Lemma weak_until_until_or_always :
 Proof.
 intros J P s.
 case (classic (eventually P s)).
-  intros evP wu.
+- intros evP wu.
   left.
   induction evP.
-    apply U0. assumption.
-  apply weak_until_Cons in wu.
-  case wu.
-    intros PC.
-    apply U0. assumption.
-  intros [Js wu'].
-  apply U_next; trivial.
-  apply IHevP.
-  assumption.
-intros evP wu.
-right.
-apply not_eventually_always_not in evP.
-apply weak_until_always_not_always in wu; trivial.
+  * apply U0. assumption.
+  * apply weak_until_Cons in wu.
+    case wu.
+    + intros PC.
+      apply U0. assumption.
+    + intros [Js wu'].
+      apply U_next; trivial.
+      apply IHevP.
+      assumption.
+- intros evP wu.
+  right.
+  apply not_eventually_always_not in evP.
+  apply weak_until_always_not_always in wu; trivial.
 Qed.
 
 Lemma not_until_weak_until :
@@ -37,24 +37,24 @@ intros J P.
 cofix c.
 intros s.
 case (classic (P s)).
-  intros Ps un.
+- intros Ps un.
   contradict un.
   apply U0.
   assumption.
-intros Ps.
-case (classic (J s)); destruct s as [x s].
-  intros Js un.
-  apply W_tl.
-    unfold and_tl, not_tl.
+- intros Ps.
+  case (classic (J s)); destruct s as [x s].
+  * intros Js un.
+    apply W_tl.
+    + unfold and_tl, not_tl.
+      split; trivial.
+    + simpl.
+      apply c.
+      intros unn.
+      contradict un.
+      apply U_next; trivial.
+  * intros Js un.
+    apply W0.
     split; trivial.
-  simpl.
-  apply c.
-  intros unn.
-  contradict un.
-  apply U_next; trivial.
-intros Js un.
-apply W0.
-split; trivial.
 Qed.
 
 Lemma not_weak_until_until :
@@ -69,23 +69,23 @@ revert s un.
 cofix c.
 intros s.
 case (classic (P s)).
-  intros Ps un.
+- intros Ps un.
   apply W0.
   assumption.
-intros Ps.
-case (classic (J s)); destruct s as [x s].
-  intros Js un.
-  apply W_tl; trivial.
-  simpl.
-  apply c.
-  intros unn.
-  contradict un.
-  apply U_next; trivial.
-  split; trivial.
-intros Js un.
-contradict un.
-apply U0.
-split; trivial.
+- intros Ps.
+  case (classic (J s)); destruct s as [x s].
+  * intros Js un.
+    apply W_tl; trivial.
+    simpl.
+    apply c.
+    intros unn.
+    contradict un.
+    apply U_next; trivial.
+    split; trivial.
+  * intros Js un.
+    contradict un.
+    apply U0.
+    split; trivial.
 Qed.
 
 Lemma not_eventually_not_always : 
@@ -98,17 +98,17 @@ intro s.
 destruct s as [e s].
 intros evnP.
 apply Always.
-  case (classic (P (Cons e s))); trivial.
+- case (classic (P (Cons e s))); trivial.
   intros orP.
   apply (E0 _ (~_ P)) in orP.
   contradict evnP.
   assumption.
-apply c.
-simpl.
-intros evP.
-contradict evnP.
-apply E_next.
-assumption.
+- apply c.
+  simpl.
+  intros evP.
+  contradict evnP.
+  apply E_next.
+  assumption.
 Qed.
 
 Lemma not_always_eventually_not : 
@@ -131,27 +131,27 @@ intros J P.
 cofix c.
 intros s.
 case (classic (J s)).
-  intros Js un.
+- intros Js un.
   destruct s as [x s].
   apply R0; trivial.
-  case (classic (P (Cons x s))); trivial.
-  intros Ps.
-  contradict un.
-  apply U0.
-  apply Ps.  
-intros Js un.
-destruct s as [x s].
-apply R_tl.
   case (classic (P (Cons x s))); trivial.
   intros Ps.
   contradict un.
   apply U0.
   apply Ps.
-simpl.
-apply c.
-intros unn.
-contradict un.
-apply U_next; trivial.
+- intros Js un.
+  destruct s as [x s].
+  apply R_tl.
+  * case (classic (P (Cons x s))); trivial.
+    intros Ps.
+    contradict un.
+    apply U0.
+    apply Ps.
+  * simpl.
+    apply c.
+    intros unn.
+    contradict un.
+    apply U_next; trivial.
 Qed.
 
 Lemma not_release_until :
@@ -166,23 +166,23 @@ revert s un.
 cofix c.
 intros s un.
 case (classic (P s)).
-  intros Ps.
+- intros Ps.
   contradict un.
   apply U0.
   assumption.
-intros Ps.
-case (classic (J s)).
-  intros Js.
-  destruct s as [x s].
-  apply R_tl; trivial.
-  simpl.
-  apply c.
-  intros unn.
-  contradict un.
-  apply U_next; trivial.
-intros Js.
-destruct s as [x s].
-apply R0; unfold not_tl; assumption.
+- intros Ps.
+  case (classic (J s)).
+  * intros Js.
+    destruct s as [x s].
+    apply R_tl; trivial.
+    simpl.
+    apply c.
+    intros unn.
+    contradict un.
+    apply U_next; trivial.
+  * intros Js.
+    destruct s as [x s].
+    apply R0; unfold not_tl; assumption.
 Qed.
 
 Lemma not_inf_often_continuously_not : 
@@ -192,11 +192,11 @@ Proof.
 intros P s ioP.
 apply not_always_eventually_not in ioP.
 induction ioP.
-  apply not_eventually_always_not in H.
+- apply not_eventually_always_not in H.
   apply E0.
   assumption.
-apply E_next.
-assumption.
+- apply E_next.
+  assumption.
 Qed.
 
 Lemma not_continously_inf_often_not :
@@ -207,17 +207,17 @@ intros P.
 cofix c.
 intros [x s] cnyP.
 apply Always.
-  unfold continuously in cnyP.
+- unfold continuously in cnyP.
   apply not_eventually_always_not in cnyP.
   apply always_now in cnyP.
   unfold not_tl in cnyP.
   apply not_always_eventually_not in cnyP.
   assumption.
-apply c.
-intros cnynP.
-contradict cnyP.
-apply E_next.
-assumption.
+- apply c.
+  intros cnynP.
+  contradict cnyP.
+  apply E_next.
+  assumption.
 Qed.
 
 Lemma not_tl_and_tl_or_tl :

exteq.v

@@ -73,8 +73,8 @@ Lemma extensional_or_tl :
   extensional P -> extensional Q -> extensional (P \/_ Q).
 Proof. 
 intros P Q eP eQ s1 s2 e. destruct e; simpl. unfold or_tl. intuition.
-  left; apply eP with (Cons x s1); [constructor; assumption | assumption]. 
-  right; apply eQ with (Cons x s1); [constructor; assumption | assumption]. 
+- left; apply eP with (Cons x s1); [constructor; assumption | assumption]. 
+- right; apply eQ with (Cons x s1); [constructor; assumption | assumption]. 
 Qed.
 
 Lemma extensional_impl_tl :
@@ -83,10 +83,10 @@ Lemma extensional_impl_tl :
 Proof. 
 intros P Q eP eQ s1 s2 e. destruct e; simpl. unfold impl_tl. 
 intros PQ1 P2. 
-  apply eQ with (Cons x s1); [constructor; assumption | idtac]. 
-  apply PQ1. apply eP with (Cons x s2). 
-    constructor. apply exteq_sym. assumption. 
-    assumption. 
+apply eQ with (Cons x s1); [constructor; assumption | idtac].
+apply PQ1. apply eP with (Cons x s2). 
+- constructor. apply exteq_sym. assumption.
+- assumption.
 Qed.
 
 Lemma extensional_not_tl :
@@ -126,10 +126,10 @@ Lemma extensional_always :
   forall (P: infseq T -> Prop),
   extensional P -> extensional (always P).
 Proof.
-intros P eP. cofix cf. 
-intros (x1, s1) (x2, s2) e al1. case (always_Cons al1); intros Px1s1 als1. constructor. 
-  eapply eP; eassumption. 
-  simpl. apply cf with s1; try assumption. case (exteq_inversion e); trivial.
+intros P eP. cofix cf.
+intros (x1, s1) (x2, s2) e al1. case (always_Cons al1); intros Px1s1 als1. constructor.
+- eapply eP; eassumption. 
+- simpl. apply cf with s1; try assumption. case (exteq_inversion e); trivial.
 Qed.
 
 Lemma extensional_weak_until :
@@ -138,10 +138,10 @@ Lemma extensional_weak_until :
 Proof.
 intros P Q eP eQ. cofix cf. 
 intros (x1, s1) (x2, s2) e un1. case (weak_until_Cons un1).
-  intro Q1. constructor 1. eapply eQ; eassumption.
-  intros (Px1s1, uns1). constructor 2.
-    eapply eP; eassumption. 
-    simpl. apply cf with s1; try assumption. case (exteq_inversion e); trivial.
+- intro Q1. constructor 1. eapply eQ; eassumption.
+- intros (Px1s1, uns1). constructor 2.
+  * eapply eP; eassumption. 
+  * simpl. apply cf with s1; try assumption. case (exteq_inversion e); trivial.
 Qed.
 
 Lemma extensional_until :
@@ -150,12 +150,12 @@ Lemma extensional_until :
 Proof.
 intros P Q eP eQ s1 s2 e un1; genclear e; genclear s2.
 induction un1.
-  intros s2 e; apply U0; apply eQ with s; assumption.
-intros (x2, s2) e.
-apply U_next.
-  apply eP with (Cons x s); assumption.
-apply IHun1.
-case (exteq_inversion e). trivial.
+- intros s2 e; apply U0; apply eQ with s; assumption.
+- intros (x2, s2) e.
+  apply U_next.
+  * apply eP with (Cons x s); assumption.
+  * apply IHun1.
+    case (exteq_inversion e). trivial.
 Qed.
 
 Lemma extensional_release :
@@ -164,12 +164,12 @@ Lemma extensional_release :
 Proof.
 intros P Q eP eQ. cofix cf. 
 intros (x1, s1) (x2, s2) e rl1. case (release_Cons rl1). intros Qx orR. case orR; intro orRx.
-  apply R0.
-    eapply eQ; eassumption.
-    eapply eP; eassumption.
-  apply R_tl.
-    eapply eQ; eassumption.
-    simpl. apply cf with s1; trivial. case (exteq_inversion e); trivial.
+- apply R0.
+  * eapply eQ; eassumption.
+  * eapply eP; eassumption.
+- apply R_tl.
+  * eapply eQ; eassumption.
+  * simpl. apply cf with s1; trivial. case (exteq_inversion e); trivial.
 Qed.
 
 Lemma extensional_eventually :
@@ -178,9 +178,9 @@ Lemma extensional_eventually :
 Proof.
 intros P eP s1 s2 e ev1. genclear e; genclear s2.
 induction ev1 as [s1 ev1 | x1 s1 ev1 induc_hyp].
-  intros s2 e. constructor 1. apply eP with s1; assumption.
-  intros (x2, s2) e. constructor 2. apply induc_hyp.
-    case (exteq_inversion e). trivial.
+- intros s2 e. constructor 1. apply eP with s1; assumption.
+- intros (x2, s2) e. constructor 2. apply induc_hyp.
+  case (exteq_inversion e). trivial.
 Qed.
 
 Lemma extensional_inf_often :