proposition: Theorem DeductionTheorem : forall (T : System) (f g : Formula) (prf : SysPrf (Ensembles.Add _ T g) f), SysPrf T (g -> f)%fol.
proof: Proof. intros T; assert (EasyCase : forall (g z : Formula), Prf nil z -> SysPrf (fun x : Formula => In x nil /\ mem _ T x) (g -> z)%fol). { intros g z H. set (A1 := IMP1 L z g) in *. set (A2 := MP L _ _ _ _ A1 H) in *. exists (nil:list Formula). exists A2. intros g0 H0; elim H0. } intros f g [F [t HF]]. assert (H0: SysPrf (fun x => In x F /\ mem _ T x) (g -> f)%fol). { induction t as [A | Axm1 Axm2 A B H1 HrecH1 H0 HrecH0 | Axm A v n H HrecH | A B | A B C | A B | A v t | A v n | A B v | | | | R | f]. - pose (m := HF _ (or_introl _ (refl_equal A))). clearbody m. destruct m. + set (A1 := AXM L x) in *. set (A2 := IMP1 L x g) in *. set (A3 := MP L _ _ _ _ A2 A1) in *. exists (x :: nil). exists A3. intros g0 H0; split. * apply H0. * destruct H0 as [H0 | H0]. -- now subst. -- contradiction. + destruct H. set (A1 := IMP2 L g (g -> g)%fol g) in *. set (A2 := IMP1 L g (g -> g)%fol) in *. set (A3 := MP L _ _ _ _ A1 A2) in *. set (A4 := IMP1 L g g) in *. set (A5 := MP L _ _ _ _ A3 A4) in *. exists (nil:list Formula); exists A5; contradiction. - induction HrecH0 as (x, H). + induction H as (x0, H). induction HrecH1 as (x1, H2). * induction H2 as (x2, H2). set (A1 := IMP2 L g A B) in *. set (A2 := MP L _ _ _ _ A1 x2) in *. set (A3 := MP L _ _ _ _ A2 x0) in *. exists (x1 ++ x). exists A3. simpl in |- *. clear - H H2. intros g H0; split. -- change (In g (Axm1 ++ Axm2)); apply in_or_app. destruct (in_app_or _ _ _ H0); firstorder. -- destruct (in_app_or _ _ _ H0); firstorder. * firstorder auto with datatypes. + firstorder auto with datatypes. - induction HrecH as (x, H0). + induction H0 as (x0, H0). assert (H1: In g Axm \/ (forall x, In x Axm -> mem _ T x)). { clear - HF. induction Axm. - firstorder. - elim (HF a (or_introl _ (refl_equal a))). assert (H :forall g0 : fol.Formula L, In g0 Axm -> mem (fol.Formula L) (Ensembles.Add (fol.Formula L) T g) g0) by firstorder. + destruct (IHAxm H). * firstorder. * intros; right. intros x0 [H2|H2]. -- elim H2; assumption. -- apply H0; assumption. + intros x H; elim H. firstorder. } destruct H1 as [a|b]. * assert (~ In v (freeVarListFormula L x)). { clear x0 H. induction x as [| a0 x Hrecx]. - auto. - unfold not in |- *; intro H; simpl in H. induction (in_app_or _ _ _ H). + elim n. eapply In_freeVarListFormula. * apply H1. * firstorder. + elim Hrecx. * intros. apply H0. firstorder. * assumption. } assert (H2: ~ In v (freeVarF g)). { unfold not in |- *; intros; elim n. eapply In_freeVarListFormula. apply H2. assumption. } set (A1 := GEN L _ _ _ H1 x0) in *. set (A2 := FA3 L g A v) in *. set (A3 := MP L _ _ _ _ A2 A1) in *. set (A4 := FA2 L g v H2) in *. set (A5 := IMP2 L g (allH v, g)%fol (allH v, A)%fol) in *. set (A6 := IMP1 L ((allH v, g) -> (allH v, A))%fol g) in *. set (A7 := MP L _ _ _ _ A6 A3) in *. set (A8 := MP L _ _ _ _ A5 A7) in *. set (A9 := MP L _ _ _ _ A8 A4) in *. exists (x ++ nil). exists A9. clear A9 A8 A7 A6 A5 A4 A3 A2 A1. simpl in |- *. intros g0 H3; apply H0. induction (in_app_or _ _ _ H3). -- auto. -- elim H4. * set (A1 := GEN L _ _ _ n H) in *. set (A2 := IMP1 L (allH v, A)%fol g) in *. set (A3 := MP L _ _ _ _ A2 A1) in *. exists (Axm). exists A3. firstorder. + firstorder. - apply EasyCase, (IMP1 L). - apply EasyCase, (IMP2 L). - apply EasyCase, (CP L). - apply EasyCase, (FA1 L). - apply EasyCase, (FA2 L); assumption. - apply EasyCase, (FA3 L). - apply EasyCase, (EQ1 L). - apply EasyCase, (EQ2 L). - apply EasyCase, (EQ3 L). - apply EasyCase, (EQ4 L). - apply EasyCase, (EQ5 L). } destruct H0 as [x [x0 H0]]; exists x, x0; firstorder. Qed.
imports: Coq(Ensembles List) hydras.Ackermann(folProof folProp)