proposition: Lemma liftCloseFrom (n : nat) : forall(f : fol.Formula L) (T : fol.System L) (m : nat), (forall v : nat, In v (freeVarF f) -> v < m) -> n <= m -> folProof.SysPrf L T (closeFrom 0 n f) -> folProof.SysPrf L T (closeFrom m n (subAllFormula f (fun x : nat => match le_lt_dec n x with | left _ => var x | right _ => var (m + x) end))).
proof: Proof. induction n as [| n Hrecn]; simpl. - intros; replace (subAllFormula f (fun x : nat => match le_lt_dec 0 x with | left _ => var x | right _ => var (m + x) end)) with (subAllFormula f (fun x : nat => var x)). + apply (impE L) with f. * apply (iffE2 L). apply subAllFormulaId. * apply H1. + apply subAllFormula_ext. intros m0 H2; induction (le_lt_dec 0 m0) as [? | b]. * reflexivity. * elim (Nat.nlt_0_r _ b). - intros f T m H H0 H1; apply (impE L) with (forallH n (closeFrom 0 n f)). + apply sysExtend with (Empty_set (fol.Formula L)). * intros x H2; contradiction H2. * apply (impI L); apply (forallI L). -- intros [x [H2 H3]]; destruct H3 as [x H3| x H3]; destruct H3. assert (H3:forall q : nat, n <= q -> m <= q -> ~ In q (freeVarF (forallH n (closeFrom 0 n f)))). { clear H2 H1 T Hrecn. induction n as [| n Hrecn]; simpl in |- *. - intros q H1 H2 H3; assert (H': q < m). { apply H; eapply in_remove; apply H3; lia. } lia. - intros q H1 H2 H3; elim Hrecn with (q := q). + apply le_S_n. apply le_S. auto. + apply le_S_n. apply le_S. auto. + auto. + simpl; eapply in_remove. apply H3. } apply H3 with (q := m + n). ++ apply Compat815.le_plus_r. ++ apply Nat.le_add_r. ++ apply H2. -- apply (impE L) with (closeFrom m n (substF (subAllFormula f (fun x : nat => match le_lt_dec n x with | left _ => var x | right _ => var (m + x) end)) n (var (m + n)))). ++ apply sysWeaken; clear H1 H T Hrecn. cut (folProof.SysPrf L (Empty_set (fol.Formula L)) (impH (substF (subAllFormula f (fun x : nat => match le_lt_dec n x with | left _ => var x | right _ => var (m + x) end)) n (var (m + n))) (subAllFormula f (fun x : nat => match le_lt_dec (S n) x with | left _ => var x | right _ => var (m + x) end)))). ** generalize (substF (subAllFormula f (fun x : nat => match le_lt_dec n x with | left _ => var x | right _ => var (m + x) end)) n (var (m + n))). generalize (subAllFormula f (fun x : nat => match le_lt_dec (S n) x with | left _ => var x | right _ => var (m + x) end)). clear f H0; intros f f0 H. induction n as [| n Hrecn]; simpl. --- apply H. --- apply (impI L). apply (forallI L). intros [x [H0 H1]]; induction H1 as [x H1| x H1]; [ induction H1 | induction H1 ]. +++ now elim (in_remove_neq _ _ _ _ _ H0). +++ apply impE with (closeFrom m n f0). *** apply sysWeaken. apply Hrecn. *** eapply forallSimp. apply Axm; right; constructor. ** replace (subAllFormula f (fun x : nat => match le_lt_dec (S n) x with | left _ => var x | right _ => var (m + x) end)) with (subAllFormula f (fun x : nat => substT match le_lt_dec n x with | left _ => var x | right _ => var (m + x) end n (var (m + n)))). --- apply (iffE1 L). apply subSubAllFormula with (m := fun x : nat => match le_lt_dec n x with | left _ => var x | right _ => var (m + x) end). --- apply subAllFormula_ext. intros m0 H1; induction (le_lt_dec n m0) as [a | ?]. +++ induction (le_lt_dec (S n) m0). *** apply (subTermVar2 L); lia. *** rewrite Nat.lt_eq_cases in a. destruct a. assert False by lia; contradiction. rewrite H; apply (subTermVar1 L). +++ induction (le_lt_dec (S n) m0). lia. apply (subTermVar2 L). unfold not in |- *; intros. rewrite H in H0. rewrite Nat.le_ngt in H0. lia. ++ assert (H2: forall (f : fol.Formula L) (s r m p : nat), m < s -> s + r <= p -> folProof.SysPrf L (Empty_set (fol.Formula L)) (impH (substF (closeFrom s r f) m (var p)) (closeFrom s r (substF f m (var p))))). { clear H0 H H1 m T f n Hrecn. intros f s n. induction n as [| n Hrecn]; simpl. - intros m p H H0; apply (impRefl L). - intros m p H H0; rewrite (subFormulaForall L). induction (eq_nat_dec (s + n) m) as [a | b]. + rewrite <- a in H; lia. + induction (In_dec eq_nat_dec (s + n) (freeVarT (var p))) as [a | ?]. * induction a as [H1| H1]. -- rewrite Nat.add_succ_r in H0; simpl in H0. rewrite <- H1 in H0; lia. -- contradiction. * apply (impI L). apply (forallI L). intros [x [H1 H2]]; induction H2 as [x H2| x H2]; [ induction H2 | induction H2 ]. -- now elim (in_remove_neq _ _ _ _ _ H1). -- apply impE with (substF (closeFrom s n f) m (var p)). ++ apply sysWeaken. ** apply Hrecn. --- auto. --- apply le_S_n. apply le_S; lia. ++ eapply (forallSimp L). apply Axm; right; constructor. } apply (impE L) with (substF (closeFrom m n (subAllFormula f (fun x : nat => match le_lt_dec n x with | left _ => var x | right _ => var (m + x) end))) n (var (m + n))). ** apply sysWeaken, H2. --- apply H0; auto. --- auto. ** apply (forallE L). apply (impE L) with (forallH n (closeFrom 0 n f)). --- apply sysExtend with (Empty_set (fol.Formula L)). +++ intros x H3; destruct H3. +++ apply (impI L), (forallI L). *** intros [x [H3 H4]]; induction H4 as [x H4| x H4]; [ induction H4 | induction H4 ]. now elim (in_remove_neq _ _ _ _ _ H3). *** apply Hrecn. apply H. apply le_S_n. apply le_S. auto. eapply (forallSimp L). apply Axm; right; constructor. --- apply Axm; right; constructor. + apply H1. Qed.
imports: Coq(Ensembles List Arith Peano_dec) hydras.Ackermann(ListExt folProof folLogic folLogic2 folProp) hydras(folReplace subProp Compat815) Coq(Lia)