proposition: Lemma preserveValue (value : nat -> U M): (forall f : Formula L, mem _ T f -> interpFormula value (nnTranslate f)) -> forall g : Formula L, SysPrf L T g -> interpFormula value (nnTranslate g).
proof: Proof. intros H g H0. induction H0 as (x, H0). induction H0 as (x0, H0). cut (forall g : Formula L, List.In g x -> interpFormula value (nnTranslate g)). - clear H H0; revert value. induction x0 as [A| Axm1 Axm2 A B x0_1 Hrecx0_1 x0_0 Hrecx0_0| Axm A v n x0 Hrecx0| A B| A B C| A B| A v t| A v n| A B v| | | | R| f]; intros; try (simpl in |- *; tauto). + apply H. auto with datatypes. + assert (H0: interpFormula value (nnTranslate A)) by auto with datatypes. assert (H1: interpFormula value (nnTranslate (A -> B)%fol)) by auto with datatypes. clear Hrecx0_1 Hrecx0_0. simpl in H0, H1. simpl in |- *. tauto. + simpl in |- *. intros. apply H0. clear H0. intros. simpl in Hrecx0. apply (Hrecx0 (updateValue value v x)). * intros. simpl in H. eapply H. -- apply H1. -- intros. apply H2. apply freeVarInterpFormula with value. ++ intros. rewrite <- freeVarNNHelp in H4. unfold updateValue in |- *. induction (eq_nat_dec v x1). ** elim n. rewrite a. clear n x0 Hrecx0 H. induction Axm as [| a0 Axm HrecAxm]. apply H1. simpl in |- *. simpl in H1. induction H1 as [H| H]. rewrite H. auto with datatypes. auto with datatypes. ** reflexivity. ++ assumption. * assumption. + simpl in |- *. intros. apply H0. intros. elim H1 with (interpTerm value t). intros. apply H0. intros. rewrite <- subNNHelp. apply subInterpFormula1. auto. + simpl in |- *. intros. apply H0. intros. apply H2. apply freeVarInterpFormula with value. * intros. unfold updateValue in |- *. induction (eq_nat_dec v x0). -- elim n. rewrite a. rewrite freeVarNNHelp. assumption. -- reflexivity. * assumption. + simpl in |- *. intros. apply H0. clear H0. intros. apply H0 with x. intros. apply H1 with x. auto. + simpl in |- *. auto. + simpl in |- *. intros. apply H0. intros. transitivity (value 1); auto. + simpl in |- *. intros. apply H0. clear H H0. unfold AxmEq4 in |- *. cut (forall a b : Terms L (arityR L R), interpTermsVector value _ a = interpTermsVector value _ b -> interpFormula value (nnHelp (iffH (atomic R a) (atomic R b)))). * assert (H: forall A, (forall a b : Terms L (arityR L R), interpTermsVector value (arityR L R) a = interpTermsVector value (arityR L R) b -> interpFormula value (nnHelp (A a b))) -> interpFormula value (nnHelp (nat_rec (fun _ : nat => Formula L) (prod_rec (fun _ : Terms L (arityR L R) * Terms L (arityR L R) => Formula L) (fun a b : Terms L (arityR L R) => A a b) (nVars L (arityR L R))) (fun (n : nat) (Hrecn : Formula L) => (v#(n + n)%nat = v#(S (n+n))%nat -> Hrecn)%fol) (arityR L R)))). { generalize (arityR L R). simple induction n. - simpl; intros A H; now apply H. - intros n0 H A H0; simpl; induction (nVars L n0). simpl in H |- *. intro H1; apply (H (fun x y : Terms L n0 => A (Tcons (var (n0 + n0)) x) (Tcons (var (S (n0 + n0))) y))). intros a0 b0 H2; apply H0. simpl; rewrite H1. now rewrite H2. } apply (H (fun a b => iffH (atomic R a) (atomic R b))). * simpl; generalize (rel M R). generalize (arityR L R). intros n n0 a b H H0. induction a as [| n t a Hreca]. -- assert (H1: b = Tnil) by (symmetry; apply nilTerms). rewrite H1 in H0; auto. -- induction (consTerms L n b) as [x p]. induction x as (a0, b0). simpl in p. rewrite <- p in H0. rewrite <- p in H. simpl in H. inversion H. simpl in H0. rewrite H2 in H0. apply (Hreca (n0 (interpTerm value a0)) b0). ++ apply (inj_pair2_eq_dec _ eq_nat_dec _ _ _ _ H3). ++ auto. + simpl in |- *. intros H0; apply H0. clear H H0. unfold AxmEq5 in |- *. cut (forall a b : Terms L (arityF L f), interpTermsVector value _ a = interpTermsVector value _ b -> interpFormula value (nnHelp (apply f a = apply f b)%fol)). * assert (H: forall A, (forall a b : Terms L (arityF L f), interpTermsVector value (arityF L f) a = interpTermsVector value (arityF L f) b -> interpFormula value (nnHelp (A a b))) -> interpFormula value (nnHelp (nat_rec (fun _ : nat => Formula L) (prod_rec (fun _ : Terms L (arityF L f) * Terms L (arityF L f) => Formula L) (fun a b : Terms L (arityF L f) => A a b) (nVars L (arityF L f))) (fun (n : nat) (Hrecn : Formula L) => (v#(n + n)%nat = v#(S (n + n))%nat -> Hrecn)%fol) (arityF L f)))). { generalize (arityF L f). simple induction n. - simpl; intros A H; auto. - intros n0 H A H0; simpl. induction (nVars L n0). simpl in H |- *. intros H1; apply (H (fun x y : Terms L n0 => A (Tcons (var (n0 + n0)) x) (Tcons (var (S (n0 + n0))) y))). intros a0 b0 H2; apply H0. simpl; rewrite H1. now rewrite H2. } apply (H (fun a b => equal (apply f a) (apply f b))). * simpl; generalize (func M f). generalize (arityF L f). intros n n0 a b H. induction a as [| n t a Hreca]. -- assert (H0: b = Tnil) by ( symmetry; apply nilTerms). now rewrite H0. -- induction (consTerms L n b) as [x p]; induction x as (a0, b0). simpl in p; rewrite <- p; rewrite <- p in H. simpl in H. inversion H. simpl; rewrite H1. apply Hreca. apply (inj_pair2_eq_dec _ eq_nat_dec _ _ _ _ H2). - auto. Qed.
imports: Coq(Ensembles List Vector Arith) hydras.Ackermann(ListExt folProof folProp) Coq(Peano_dec) hydras.Ackermann(misc) hydras.Ackermann(NewNotations)