diff options
Diffstat (limited to 'theories/Logic')
| -rw-r--r-- | theories/Logic/Berardi.v | 18 | ||||
| -rw-r--r-- | theories/Logic/EqdepFacts.v | 3 | ||||
| -rw-r--r-- | theories/Logic/Eqdep_dec.v | 26 | ||||
| -rw-r--r-- | theories/Logic/JMeq.v | 8 |
4 files changed, 27 insertions, 28 deletions
diff --git a/theories/Logic/Berardi.v b/theories/Logic/Berardi.v index ed4d69ab02..86894cd1f2 100644 --- a/theories/Logic/Berardi.v +++ b/theories/Logic/Berardi.v @@ -88,8 +88,8 @@ Lemma L1 : forall A B:Prop, retract_cond (pow A) (pow B). Proof. intros A B. destruct (EM (retract (pow A) (pow B))) as [(f0,g0,e) | hf]. - exists f0 g0; trivial. - exists (fun (x:pow A) (y:B) => F) (fun (x:pow B) (y:A) => F); intros; +- exists f0 g0; trivial. +- exists (fun (x:pow A) (y:B) => F) (fun (x:pow B) (y:A) => F); intros; destruct hf; auto. Qed. @@ -130,9 +130,9 @@ Proof. unfold R at 1. unfold g. rewrite AC. -trivial. -exists (fun x:pow U => x) (fun x:pow U => x). -trivial. +- trivial. +- exists (fun x:pow U => x) (fun x:pow U => x). + trivial. Qed. @@ -141,11 +141,11 @@ Proof. generalize not_has_fixpoint. unfold Not_b. apply AC_IF. -intros is_true is_false. -elim is_true; elim is_false; trivial. +- intros is_true is_false. + elim is_true; elim is_false; trivial. -intros not_true is_true. -elim not_true; trivial. +- intros not_true is_true. + elim not_true; trivial. Qed. diff --git a/theories/Logic/EqdepFacts.v b/theories/Logic/EqdepFacts.v index 8e59941f37..b930388d13 100644 --- a/theories/Logic/EqdepFacts.v +++ b/theories/Logic/EqdepFacts.v @@ -372,8 +372,7 @@ Proof. rewrite (UIP_refl y). intros z. assert (UIP:forall y' y'' : x = x, y' = y''). - { intros. apply eq_trans with (eq_refl x). apply UIP_refl. - symmetry. apply UIP_refl. } + { intros. apply eq_trans_r with (eq_refl x); apply UIP_refl. } transitivity (eq_trans (eq_trans (UIP (eq_refl x) (eq_refl x)) z) (eq_sym (UIP (eq_refl x) (eq_refl x)))). - destruct z. destruct (UIP _ _). reflexivity. diff --git a/theories/Logic/Eqdep_dec.v b/theories/Logic/Eqdep_dec.v index 4e8b48af9f..3babc9437b 100644 --- a/theories/Logic/Eqdep_dec.v +++ b/theories/Logic/Eqdep_dec.v @@ -66,9 +66,9 @@ Section EqdepDec. intros. unfold nu. destruct (eq_dec y) as [Heq|Hneq]. - reflexivity. + - reflexivity. - case Hneq; trivial. + - case Hneq; trivial. Qed. @@ -118,15 +118,15 @@ Section EqdepDec. Proof. intros. cut (proj (ex_intro P x y) y = proj (ex_intro P x y') y). - simpl. - destruct (eq_dec x) as [Heq|Hneq]. - elim Heq using K_dec_on; trivial. + - simpl. + destruct (eq_dec x) as [Heq|Hneq]. + + elim Heq using K_dec_on; trivial. - intros. - case Hneq; trivial. + + intros. + case Hneq; trivial. - case H. - reflexivity. + - case H. + reflexivity. Qed. End EqdepDec. @@ -163,8 +163,8 @@ Theorem K_dec_type : Proof. intros A eq_dec x P H p. elim p using K_dec; intros. - case (eq_dec x0 y); [left|right]; assumption. - trivial. + - case (eq_dec x0 y); [left|right]; assumption. + - trivial. Qed. Theorem K_dec_set : @@ -260,8 +260,8 @@ Module DecidableEqDep (M:DecidableType). Proof. intros. apply inj_right_pair with (A:=U). - intros x0 y0; case (eq_dec x0 y0); [left|right]; assumption. - assumption. + - intros x0 y0; case (eq_dec x0 y0); [left|right]; assumption. + - assumption. Qed. End DecidableEqDep. diff --git a/theories/Logic/JMeq.v b/theories/Logic/JMeq.v index 3914f44a2c..11897b6cb1 100644 --- a/theories/Logic/JMeq.v +++ b/theories/Logic/JMeq.v @@ -135,10 +135,10 @@ Proof. exists bool. exists (fun _ => True). exists true. exists false. exists I. exists I. split. -trivial. -intro H. -assert (true=false) by (destruct H; reflexivity). -discriminate. +- trivial. +- intro H. + assert (true=false) by (destruct H; reflexivity). + discriminate. Qed. (** However, when the dependencies are equal, [JMeq (P p) x (P q) y] |