Commit 93bf716d by Samuel Ben Hamou

### ModusPonens dans le bon sens.

parent 846f9704
 ... ... @@ -97,7 +97,7 @@ Hint Unfold IsTheorem IsTheoremStrict. (** A theorem to build proofs using former lemmas. *) Lemma ModusPonens th : forall A B , IsTheorem th (A -> B) -> IsTheorem th A -> IsTheorem th B. Lemma ModusPonens th : forall A B , IsTheorem th A -> IsTheorem th B -> IsTheorem th (A -> B). Proof. intros. unfold IsTheorem in *. ... ... @@ -105,7 +105,7 @@ Proof. split. + unfold Wf in *. intuition. * assert (check th (A -> B)%form = true -> check th B = true). * assert (check th A = true /\ check th B = true -> check th (A -> B)%form = true). { assert (check th (A -> B)%form = check th A && check th B). { auto. } ... ... @@ -113,37 +113,33 @@ Proof. { apply andb_lazy_alt. } rewrite H8 in H5. intro. rewrite H5 in H9. assert (check th A = true /\ check th B = true). { apply andb_true_iff. rewrite H8. assumption. } destruct H10. rewrite H5. apply andb_true_iff. assumption. } apply H5. assumption. * assert (BClosed (A -> B)%form -> BClosed A /\ BClosed B). apply H5. split; assumption. * assert (BClosed A /\ BClosed B -> BClosed (A -> B)%form). { intro. unfold BClosed in *. cbn in H5. apply max_0 in H5. cbn. apply max_0. assumption. } apply H5 in H0. destruct H0. assumption. * assert (FClosed (A -> B)%form -> FClosed A /\ FClosed B). apply H5. split; assumption. * assert (FClosed A /\ FClosed B -> FClosed (A -> B)%form). { intro. unfold FClosed in *. cbn in H5. assert (forall s s', Names.Empty (Names.union s s') -> Names.Empty s /\ Names.Empty s'). { split. namedec. namedec. } cbn. assert (forall s s', Names.Empty (Names.union s s') <-> Names.Empty s /\ Names.Empty s'). { split. split; namedec. namedec. } eapply H8 in H5. assumption. } apply H5 in H6. destruct H6. assumption. apply H5. split; assumption. + destruct H1. destruct H2. exists (x ++ x0). ... ... @@ -159,25 +155,15 @@ Proof. ++ apply IHl. inversion H5. assumption. } apply H5; assumption. * apply R_Imp_e with (A := A). - apply Pr_weakening with (s := x ⊢ A -> B); auto. apply SubSeq. assert (forall A (x : list A) x0, ListSubset x (x ++ x0)). { intros. induction x1. ++ unfold ListSubset. intros. inversion H5. ++ unfold ListSubset. intros. inversion H5. ** rewrite H6. simpl. apply in_eq. ** simpl. right. apply IHx1. assumption. } apply H5. - apply Pr_weakening with (s := x0 ⊢ A); auto. * apply R_Imp_i. apply Pr_weakening with (s := x0 ⊢ B); auto. apply SubSeq. assert (forall A (x : list A) x0, ListSubset x0 (x ++ x0)). { intros. induction x1. ++ unfold ListSubset. intros. simpl. assumption. ++ unfold ListSubset. intros. unfold ListSubset in IHx1. simpl. right. apply IHx1. assumption. } apply H5. apply H5 with (x := A :: x). Qed. (** We can "fix" a proof made with things not in the signature, ... ...
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment