added proof using annotations for quick compilation, added quick task to Makefile

Author: palmskog

Makefile

@@ -7,11 +7,14 @@ endif
 default: Makefile.coq
 	$(MAKE) -f Makefile.coq
 
+quick: Makefile.coq
+	$(MAKE) -f Makefile.coq quick
+
 Makefile.coq: _CoqProject
 	coq_makefile -f _CoqProject -o Makefile.coq
 
 clean:
 	$(MAKE) -f Makefile.coq clean
 	rm Makefile.coq
 
-.PHONY: default clean
+.PHONY: default clean quick

classical.v

@@ -8,7 +8,7 @@ Variable T : Type.
 Lemma weak_until_until_or_always :
   forall (J P : infseq T -> Prop) (s : infseq T),
     weak_until J P s -> until J P s \/ always J s.
-Proof.
+Proof using.
 intros J P s.
 case (classic (eventually P s)).
 - intros evP wu.
@@ -32,7 +32,7 @@ Qed.
 Lemma not_until_weak_until :
   forall (J P : infseq T -> Prop) (s : infseq T),
     ~ until J P s -> weak_until (J /\_ ~_ P) (~_ J /\_ ~_ P) s.
-Proof.
+Proof using.
 intros J P.
 cofix c.
 intros s.
@@ -60,7 +60,7 @@ Qed.
 Lemma not_weak_until_until :
   forall (J P : infseq T -> Prop) (s : infseq T),
     ~ weak_until J P s -> until (J /\_ ~_ P) (~_ J /\_ ~_ P) s.
-Proof.
+Proof using.
 intros J P s wun.
 case (classic (until (J /\_ ~_ P) (~_ J /\_ ~_ P) s)); trivial.
 intros un.
@@ -91,7 +91,7 @@ Qed.
 Lemma not_eventually_not_always : 
   forall (P : infseq T -> Prop) (s : infseq T),
   ~ eventually (~_ P) s -> always P s.
-Proof.
+Proof using.
 intros P.
 cofix c.
 intro s.
@@ -114,7 +114,7 @@ Qed.
 Lemma not_always_eventually_not : 
   forall (P : infseq T -> Prop) (s : infseq T),
   ~ always P s -> eventually (~_ P) s.
-Proof.
+Proof using.
 intros P s alP.
 case (classic ((eventually (~_ P)) s)); trivial.
 intros evP.
@@ -126,7 +126,7 @@ Qed.
 Lemma not_until_release : 
   forall (J P : infseq T -> Prop) (s : infseq T),
   ~ until (~_ J) (~_ P) s -> release J P s.
-Proof.
+Proof using.
 intros J P.
 cofix c.
 intros s.
@@ -157,7 +157,7 @@ Qed.
 Lemma not_release_until :
   forall (J P : infseq T -> Prop) (s : infseq T),
   ~ release (~_ J) (~_ P) s -> until J P s.
-Proof.
+Proof using.
 intros J P s rl.
 case (classic (until J P s)); trivial.
 intros un.
@@ -188,7 +188,7 @@ Qed.
 Lemma not_inf_often_continuously_not : 
   forall (P : infseq T -> Prop) (s : infseq T),
   ~ inf_often P s -> continuously (~_ P) s.
-Proof.
+Proof using.
 intros P s ioP.
 apply not_always_eventually_not in ioP.
 induction ioP.
@@ -202,7 +202,7 @@ Qed.
 Lemma not_continously_inf_often_not :
   forall (P : infseq T -> Prop) (s : infseq T),
   ~ continuously P s -> inf_often (~_ P) s.
-Proof.
+Proof using.
 intros P.
 cofix c.
 intros [x s] cnyP.
@@ -223,7 +223,7 @@ Qed.
 Lemma not_tl_and_tl_or_tl :
   forall (P Q : infseq T -> Prop) (s : infseq T),
   (~_ (P /\_ Q)) s -> ((~_ P) \/_ (~_ Q)) s.
-Proof.
+Proof using.
 intros P Q s; unfold not_tl, and_tl, or_tl.
 apply not_and_or.
 Qed.

exteq.v

@@ -13,26 +13,26 @@ CoInductive exteq : infseq T -> infseq T -> Prop :=
 Lemma exteq_inversion :
   forall (x1:T) s1 x2 s2, 
   exteq (Cons x1 s1) (Cons x2 s2) -> x1 = x2 /\ exteq s1 s2.
-Proof.
+Proof using.
 intros x1 s1 x2 s2 e. 
 change (hd (Cons x1 s1) = hd (Cons x2 s2) /\
         exteq (tl (Cons x1 s1)) (tl (Cons x2 s2))).
 case e; clear e x1 s1 x2 s2. simpl. intros; split; trivial. 
 Qed.
 
 Lemma exteq_refl : forall s, exteq s s. 
-Proof.
+Proof using.
 cofix cf. intros (x, s). constructor. apply cf. 
 Qed.
 
 Lemma exteq_sym : forall s1 s2, exteq s1 s2 -> exteq s2 s1.
-Proof.
+Proof using.
 cofix cf. destruct 1. constructor. apply cf. assumption. 
 Qed.
 
 Lemma exteq_trans :
    forall s1 s2 s3, exteq s1 s2 -> exteq s2 s3 -> exteq s1 s3.
-Proof.
+Proof using.
 cofix cf.
 intros (x1, s1) (x2, s2) (x3, s3) e12 e23. 
 case (exteq_inversion _ _ _ _ e12); clear e12; intros e12 ex12. 
@@ -61,20 +61,20 @@ Definition extensional (P: infseq T -> Prop) :=
 
 Lemma extensional_True_tl :
   extensional True_tl.
-Proof.
+Proof using.
 intros s1 s2 eq; auto.
 Qed.
 
 Lemma extensional_False_tl :
   extensional False_tl.
-Proof.
+Proof using.
 intros s1 s2 eq; auto.
 Qed.
 
 Lemma extensional_and_tl :
   forall (P Q: infseq T -> Prop), 
   extensional P -> extensional Q -> extensional (P /\_ Q).
-Proof. 
+Proof using. 
 intros P Q eP eQ s1 s2 e. destruct e; simpl. unfold and_tl. intuition.
 - apply eP with (Cons x s1); [constructor; assumption | assumption].
 - apply eQ with (Cons x s1); [constructor; assumption | assumption].
@@ -83,7 +83,7 @@ Qed.
 Lemma extensional_or_tl :
   forall (P Q: infseq T -> Prop),
   extensional P -> extensional Q -> extensional (P \/_ Q).
-Proof. 
+Proof using. 
 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]. 
@@ -92,7 +92,7 @@ Qed.
 Lemma extensional_impl_tl :
   forall (P Q: infseq T -> Prop),
   extensional P -> extensional Q -> extensional (P ->_ Q).
-Proof. 
+Proof using. 
 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].
@@ -104,7 +104,7 @@ Qed.
 Lemma extensional_not_tl :
   forall (P: infseq T -> Prop),
   extensional P -> extensional (~_ P).
-Proof.
+Proof using.
 intros P eP s1 s2 e; destruct e; simpl. unfold not_tl.
 intros P1 nP2.
 contradict P1.
@@ -116,28 +116,28 @@ Qed.
 
 Lemma extensional_now :
   forall (P: T -> Prop), extensional (now P).
-Proof. 
+Proof using. 
 intros P s1 s2 e. destruct e; simpl. trivial.
 Qed.
 
 Lemma extensional_next :
   forall (P: infseq T -> Prop), 
   extensional P -> extensional (next P).
-Proof.
+Proof using.
 intros P eP s1 s2 exP; destruct exP; simpl.
 apply eP; assumption.
 Qed.
 
 Lemma extensional_consecutive :
   forall (P: T -> T -> Prop), extensional (consecutive P).
-Proof. 
+Proof using. 
 intros P s1 s2 e. do 2 destruct e; simpl. trivial.
 Qed.
 
 Lemma extensional_always :
   forall (P: infseq T -> Prop),
   extensional P -> extensional (always P).
-Proof.
+Proof using.
 intros P eP. cofix cf.
 intros (x1, s1) (x2, s2) e al1. case (always_Cons al1); intros Px1s1 als1. constructor.
 - eapply eP; eassumption. 
@@ -147,7 +147,7 @@ Qed.
 Lemma extensional_weak_until :
   forall (P Q: infseq T -> Prop),
   extensional P -> extensional Q -> extensional (weak_until P Q).
-Proof.
+Proof using.
 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.
@@ -159,7 +159,7 @@ Qed.
 Lemma extensional_until :
   forall (P Q: infseq T -> Prop),
   extensional P -> extensional Q -> extensional (until P Q).
-Proof.
+Proof using.
 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.
@@ -173,7 +173,7 @@ Qed.
 Lemma extensional_release :
   forall (P Q: infseq T -> Prop),
   extensional P -> extensional Q -> extensional (release P Q).
-Proof.
+Proof using.
 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.
@@ -187,7 +187,7 @@ Qed.
 Lemma extensional_eventually :
   forall (P: infseq T -> Prop),
   extensional P -> extensional (eventually P).
-Proof.
+Proof using.
 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.
@@ -198,14 +198,14 @@ Qed.
 Lemma extensional_inf_often :
 forall (P: infseq T -> Prop),
   extensional P -> extensional (inf_often P).
-Proof.
+Proof using.
 intros P eP; apply extensional_always; apply extensional_eventually; assumption.
 Qed.
 
 Lemma extensional_continuously :
 forall (P: infseq T -> Prop),
   extensional P -> extensional (continuously P).
-Proof.
+Proof using.
 intros P eP; apply extensional_eventually; apply extensional_always; assumption.
 Qed.