diff options
| author | Pierre-Marie Pédrot | 2019-02-04 15:00:13 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-02-04 15:00:13 +0100 |
| commit | 79c87ab3ec6e41bbc5fe2cc43edcb4b934b81e46 (patch) | |
| tree | 18ce7b34d9865b5c4446f1ff6505e6682c80650c /theories/Init | |
| parent | 127f1fe146264a87d7a8cb04ab8ea34201b5c93a (diff) | |
| parent | f53a011ac83fa820faba970109485780715e153f (diff) | |
Merge PR #9386: Pass some files to strict focusing mode.
Reviewed-by: Zimmi48
Reviewed-by: herbelin
Reviewed-by: ppedrot
Diffstat (limited to 'theories/Init')
| -rw-r--r-- | theories/Init/Logic.v | 9 | ||||
| -rw-r--r-- | theories/Init/Specif.v | 5 | ||||
| -rw-r--r-- | theories/Init/Tactics.v | 8 |
3 files changed, 16 insertions, 6 deletions
diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v index 1db0a8e1b5..b607be4f94 100644 --- a/theories/Init/Logic.v +++ b/theories/Init/Logic.v @@ -383,6 +383,11 @@ Section Logic_lemmas. Register eq_trans as core.eq.trans. + Theorem eq_trans_r : x = y -> z = y -> x = z. + Proof. + destruct 2; trivial. + Defined. + Theorem f_equal : x = y -> f x = f y. Proof. destruct 1; trivial. @@ -695,8 +700,8 @@ Proof. - intros (x,(Hx,Huni)); split. + exists x; assumption. + intros x' x'' Hx' Hx''; transitivity x. - symmetry; auto. - auto. + * symmetry; auto. + * auto. Qed. Lemma forall_exists_unique_domain_coincide : diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v index cfba2bae69..e5d63c547d 100644 --- a/theories/Init/Specif.v +++ b/theories/Init/Specif.v @@ -765,8 +765,9 @@ Section Dependent_choice_lemmas. intros H x0. set (f:=fix f n := match n with O => x0 | S n' => proj1_sig (H (f n')) end). exists f. - split. reflexivity. - induction n; simpl; apply proj2_sig. + split. + - reflexivity. + - induction n; simpl; apply proj2_sig. Defined. End Dependent_choice_lemmas. diff --git a/theories/Init/Tactics.v b/theories/Init/Tactics.v index 8df533e743..af4632161e 100644 --- a/theories/Init/Tactics.v +++ b/theories/Init/Tactics.v @@ -202,13 +202,17 @@ Set Implicit Arguments. Lemma decide_left : forall (C:Prop) (decide:{C}+{~C}), C -> forall P:{C}+{~C}->Prop, (forall H:C, P (left _ H)) -> P decide. Proof. -intros; destruct decide. apply H0. contradiction. + intros; destruct decide. + - apply H0. + - contradiction. Qed. Lemma decide_right : forall (C:Prop) (decide:{C}+{~C}), ~C -> forall P:{C}+{~C}->Prop, (forall H:~C, P (right _ H)) -> P decide. Proof. -intros; destruct decide. contradiction. apply H0. + intros; destruct decide. + - contradiction. + - apply H0. Qed. Tactic Notation "decide" constr(lemma) "with" constr(H) := |