diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-03-14 21:12:31 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-03-14 21:12:31 +0100 |
| commit | 229f858e8c37b577bd07a18f3ca1e0ecd0a912fe (patch) | |
| tree | 1a16db991125ab8c3cad04ebd1c7780919579e78 /theories/Logic | |
| parent | b54892932959a3b16e31f780f7f1b638062b0a95 (diff) | |
| parent | 4ccd6436a014d5d1b27d42e9bda40fb381d1bfce (diff) | |
Merge PR#444: Simplifying a statement in Hurkens.v + a case study for eauto
Diffstat (limited to 'theories/Logic')
| -rw-r--r-- | theories/Logic/Hurkens.v | 13 |
1 files changed, 4 insertions, 9 deletions
diff --git a/theories/Logic/Hurkens.v b/theories/Logic/Hurkens.v index 56e03e965..a10c180cc 100644 --- a/theories/Logic/Hurkens.v +++ b/theories/Logic/Hurkens.v @@ -360,13 +360,12 @@ Module NoRetractToModalProposition. Section Paradox. Variable M : Prop -> Prop. -Hypothesis unit : forall A:Prop, A -> M A. -Hypothesis join : forall A:Prop, M (M A) -> M A. Hypothesis incr : forall A B:Prop, (A->B) -> M A -> M B. Lemma strength: forall A (P:A->Prop), M(forall x:A,P x) -> forall x:A,M(P x). Proof. - eauto. + intros A P h x. + eapply incr in h; eauto. Qed. (** ** The universe of modal propositions *) @@ -470,7 +469,7 @@ Hypothesis p2p2 : forall A:NProp, El A -> El (b2p (p2b A)). Theorem paradox : forall B:NProp, El B. Proof. intros B. - unshelve (refine ((fun h => _) (NoRetractToModalProposition.paradox _ _ _ _ _ _ _ _ _ _))). + unshelve (refine ((fun h => _) (NoRetractToModalProposition.paradox _ _ _ _ _ _ _ _))). + exact (fun P => ~~P). + exact bool. + exact p2b. @@ -480,8 +479,6 @@ Proof. + cbn. auto. + cbn. auto. + cbn. auto. - + auto. - + auto. Qed. End Paradox. @@ -516,7 +513,7 @@ Hypothesis p2p2 : forall A:NProp, El A -> El (b2p (p2b A)). Theorem mparadox : forall B:NProp, El B. Proof. intros B. - unshelve (refine ((fun h => _) (NoRetractToModalProposition.paradox _ _ _ _ _ _ _ _ _ _))). + unshelve (refine ((fun h => _) (NoRetractToModalProposition.paradox _ _ _ _ _ _ _ _))). + exact (fun P => P). + exact bool. + exact p2b. @@ -526,8 +523,6 @@ Proof. + cbn. auto. + cbn. auto. + cbn. auto. - + auto. - + auto. Qed. End MParadox. |