proposition: Lemma normal_forms_encodes s: normal s -> lambda lambda (ren (add 2) s) (enc 1 (var 1)) ≡ lambda lambda Succ ((ren (add 2) s) (var 1)) -> exists n, encodes s n.
proof: Proof. remember (add 2) as delta. cbn; intros H EQ % equiv_lam_elim % equiv_lam_elim; destruct s; cbn in EQ. - Injection EQ; Discriminate. - Injection EQ; Discriminate. - eapply equiv_reduce in EQ. 2, 3: dostep; asimpl; reflexivity. eapply normal_lam_elim in H. enough (exists n : nat, forall t delta, t .: delta >> var • s ≡ enc n t) as [n H'] by (exists n; intros t delta'; asimpl; rewrite stepBeta; asimpl; auto). induction s as [[] | | |]; unfold funcomp in EQ; cbn in EQ. + now (exists 0). + Discriminate. + Discriminate. + Discriminate. + eapply head_atom in H as H'; cbn; intuition. eapply equiv_app_elim in EQ as [EQ1 EQ2]; cbn; intuition. 2: eapply atom_head_lifting; auto; intros []; cbn; intuition. enough (s1 = g a). * subst. cbn in EQ2. eapply IHs2 in EQ2. 2: eauto using normal_app_r. destruct EQ2. subst. exists (S x). intros t delta; cbn; simplify; now rewrite H0. * destruct s1 as [[] | | | t1 t2]; simplify in EQ1; cbn in *. 1 - 4: try Injection EQ1; Discriminate. assert (isAtom (head (g a (var 1) .: delta >> var • t1))) by (eapply atom_head_lifting; auto; intros []; cbn; intuition). Injection EQ1. assert (isAtom (head t2)). { eapply head_atom. eauto using normal_app_r, normal_app_l. intros ?; destruct t2; cbn in H2; intuition; Discriminate. } assert (isAtom (head (g a (var 1) .: delta >> var • t2))) by (eapply atom_head_lifting; auto; intros []; cbn; intuition). destruct t1; cbn in *; try Discriminate. destruct f; cbn in *; Discriminate. destruct t2; cbn in *; try Discriminate. destruct f; cbn in *; Discriminate. Injection H1; subst. Injection H2; subst. reflexivity. - eapply normal_ren with (delta := delta) in H. eapply head_atom in H; auto. cbn in EQ. Injection EQ. Injection H0. unshelve eapply ren_equiv_proper in H2; [exact (pred >> pred)|exact (pred >> pred)|auto..]; asimpl in H2. unshelve eapply ren_equiv_proper in H3; [exact (pred >> pred)|exact (pred >> pred)|auto..]; asimpl in H3. exists 1. intros t delta'; simplify. subst delta. asimpl in H3. asimpl in H2. now rewrite H2, H3. Qed.
imports: RelationClasses Morphisms List Lia Init.Nat Setoid Undecidability.HOU(calculus.calculus second_order.diophantine_equations systemunification nth_order_unification)