From Undecidability.L Require Import Util.L_facts.
Import L_Notations.
Notation "A '.[' i ']'" := (elAt A i) (no associativity, at level 50).
Fixpoint appCross A B :=
match A with
| nil => nil
| a :: A => map (app a) B ++ appCross A B
end.
Fixpoint T n :=
match n with
| 0 => [#n]
| S n => let A := T n in A ++ [#(S n)] ++ filter (fun x => Dec (~ x el A)) ( map lam A ++ appCross A A )
end.
Lemma sublist_T : forall n : nat, exists (x : term) (B : list term), T (S n) = T n ++ x :: B.
Proof.
intros n. exists (# (S n)). simpl. eexists; reflexivity.
Qed.
Lemma T_S s n m : T n .[ m ] = Some s -> T (S n).[ m ] = Some s.
Proof.
destruct (sublist_T n) as [x [B H]]. rewrite H. eapply elAt_app.
Qed.
Lemma T_ge s n1 n2 m : n2 >= n1 -> T n1 .[ m ] = Some s -> T n2 .[ m ] = Some s.
Proof.
remember (S n1) as n1'. induction 1; inv Heqn1'; eauto using T_S.
Qed.
Lemma appCross_correct A B s t : (s el A /\ t el B) <-> (app s t) el appCross A B.
Proof.
split.
- induction A; simpl; intuition; subst; eauto using in_map.
- induction A; simpl; try rewrite in_app_iff in *; intros H; try tauto; destruct H as [H1 | H2]; intuition; rewrite in_map_iff in *; destruct H1; destruct H; [left|]; congruence.
Qed.
Lemma T_var n : #n el T n.
Proof.
destruct n; simpl; auto.
Qed.
Lemma T_app s t n : s el T n -> t el T n -> s t el T (S n).
Proof.
intros; simpl. decide (s t el T n); auto; simpl.
rewrite in_app_iff; simpl.
rewrite in_filter_iff, in_app_iff, <- appCross_correct.
intuition.
Qed.
Lemma T_el_ge s n m : n >= m -> s el T m -> s el T n.
Proof.
intros A B; destruct (el_elAt B); eapply elAt_el, T_ge; eassumption.
Qed.
Lemma T_lam s n : s el T n -> lam s el T (S n).
Proof.
intros; simpl; decide (lam s el T n); auto.
rewrite in_app_iff; simpl; rewrite in_filter_iff, in_app_iff, in_map_iff.
right. right. split; try left; eauto.
Qed.
Fixpoint exh_size s := match s with
| #n => n
| app s1 s2 => 1 + exh_size s1 + exh_size s2
| lam s => 1 + exh_size s
end.
Lemma T_exhaustive s : s el (T (exh_size s)).
Proof with
simpl; repeat rewrite in_app_iff; repeat rewrite in_filter_iff; try rewrite <- appCross_correct; eauto using in_filter_iff, in_app_iff, appCross_correct, el_elAt, elAt_el, T_ge, in_map.
induction s.
- destruct n; simpl; auto.
- eapply T_app; eapply T_el_ge; try eassumption; fold exh_size plus; lia.
- now eapply T_lam.
Qed.
Lemma T_longenough m : |T m| > m.
Proof.
induction m.
- simpl; lia.
- simpl. rewrite app_length. simpl. lia.
Qed.
Definition g s := match pos s (T (exh_size s)) with None => 0 | Some n => n end.
Definition g_inv n := match elAt (T n) n with None => #0 | Some n => n end.
Lemma g_inv_g s : g_inv (g s) = s.
Proof.
unfold g. destruct( pos s (T (exh_size s)) ) eqn:A.
unfold g_inv. destruct (T n .[ n ] ) eqn:B.
- eapply pos_elAt in A.
destruct (lt_eq_lt_dec n (exh_size s)) as [[D | D] | D].
+ eapply T_ge in B. rewrite B in A. now inv A. lia.
+ subst. assert (Some s = Some t) by now rewrite <- A, <- B. congruence.
+ eapply T_ge in A. rewrite A in B. now inv B. lia.
- eapply nth_error_none in B.
assert (|T n| > n) by eapply T_longenough. lia.
- assert (HIn : s el T (exh_size s)) by eapply T_exhaustive.
eapply el_elAt in HIn; eauto. destruct HIn. eapply elAt_el in H. eapply el_pos in H. destruct H. rewrite H in *; congruence.
Qed.
#[export] Hint Unfold left_inverse injective right_inverse surjective : core.
Lemma disjoint_symm X (A B : list X) : disjoint A B <-> disjoint B A.
Proof.
rewrite !disjoint_forall; firstorder.
Qed.
Lemma map_lam A : forall x, x el map lam A -> exists t, x = lam t.
Proof.
intros x B; rewrite in_map_iff in B; destruct B as [? [B _]]; subst; eauto.
Qed.
Lemma appCross_app A B : forall x, x el appCross A B -> exists s t, x = app s t.
Proof.
induction A.
- inversion 1.
- simpl; intros. rewrite in_app_iff in H. destruct H; eauto. rewrite in_map_iff in H. destruct H as [t [H1 H2]]; eauto; subst; eauto.
Qed.
Lemma T_var_not n m : m > n -> ~ #m el T n.
Proof.
induction n.
- destruct m; destruct 2; try lia. congruence. auto.
- simpl; intros A; rewrite !in_app_iff.
intros [H | H].
+ eapply IHn; now try lia.
+ destruct H as [H | H]. inv H; lia.
rewrite filter_app in H. rewrite in_app_iff in H.
destruct H as [H | H]; rewrite in_filter_iff in H; destruct H as [H1 H2].
* rewrite in_map_iff in H1. destruct H1 as [x [H1 _]]. inv H1.
* destruct (appCross_app H1) as [s [t H3]]; inv H3.
Qed.
Lemma appCross_dupfree A B : dupfree A -> dupfree B -> dupfree (appCross A B).
Proof with eauto using dupfree; intuition.
induction 1; intros dpf_B; simpl...
eapply dupfree_app...
-eapply disjoint_forall. intros y D Hy.
edestruct (appCross_app Hy) as [y1 [y2 Hyy]]; subst. eapply appCross_correct in Hy as [].
eapply in_map_iff in D. destruct D as [d [D1 D2]]. inv D1...
-eapply dupfree_map... congruence.
Qed.
Lemma dupfree_T : forall n, dupfree (T n).
Proof.
induction n.
- simpl. repeat econstructor. eauto.
- simpl. eapply dupfree_app.
+ eapply disjoint_symm, disjoint_cons. split.
* eapply T_var_not; lia.
* rewrite filter_app, disjoint_symm, disjoint_forall.
intros s A B. eapply in_app_iff in B. destruct B; eapply in_filter_iff in H;rewrite Dec_reflect in *;tauto.
+ eassumption.
+ eapply dupfreeC. rewrite in_filter_iff.
intros [A _]. rewrite in_app_iff in A. destruct A.
eapply map_lam in H. destruct H; inv H.
eapply appCross_app in H. destruct H as [s [t H]]. inv H.
eapply dupfree_filter. eapply dupfree_app.
rewrite disjoint_forall.
intros x A B. destruct (map_lam A), (appCross_app B) as [x1 [x2 B1]]. subst. inv B1.
eapply dupfree_map; congruence.
now eapply appCross_dupfree.
Qed.
Lemma T_dup n1 n2 m1 m2 x : T n1 .[m1 ] = Some x -> T n2 .[m2] = Some x -> m1 = m2.
Proof.
destruct (lt_eq_lt_dec n1 n2) as [[H | H] | H]; try subst;
try eapply lt_le_weak in H;
eauto using (T_ge), dupfree_elAt, dupfree_T.
Qed.
Lemma g_g_inv n : g(g_inv n) = n.
Proof.
unfold g_inv. destruct (T n .[ n ] ) eqn:B.
unfold g. destruct( pos t (T (exh_size t)) ) eqn:A.
- eapply pos_elAt, T_dup in A; eauto.
- assert (HIn : t el T (exh_size t)) by eapply T_exhaustive.
eapply el_elAt in HIn. destruct HIn.
eapply elAt_el in H. eapply el_pos in H. destruct H. rewrite H in A. congruence.
- eapply nth_error_none in B.
assert (|T n| > n) by eapply T_longenough.
lia.
Qed.
#[export] Hint Unfold left_inverse injective surjective g g_inv : core.
Lemma g_T : bijective g.
Proof.
split.
- eauto using left_inv_inj, g_inv_g.
- eauto using right_inv_surjective, g_g_inv.
Qed.
Fixpoint C (n : nat) :=
match n with
| 0 => [(0,0)]
| S n => C n ++ (S n, 0) :: filter (fun x => Dec (not (x el C n))) (map (fun p : nat * nat => let (p1,p2) := p in (p1,S p2)) (C n))
end.
Lemma sublist_C : forall n : nat, exists x B, C (S n) = C n ++ x :: B.
Proof.
repeat eexists.
Qed.
Lemma C_S p n m : C n .[ m ] = Some p -> C (S n).[ m ] = Some p.
Proof.
destruct (sublist_C n) as [x [B H]]. rewrite H. eapply elAt_app.
Qed.
Lemma C_ge p n1 n2 m : n2 >= n1 -> C n1 .[ m ] = Some p -> C n2 .[ m ] = Some p.
Proof.
remember (S n1) as n1'. induction 1; inv Heqn1'; eauto using C_S.
Qed.
Definition eSize (p : nat * nat) := let (n,m) := p in 1 + n + m.
Lemma C_exhaustive p : p el C( eSize p ).
Proof.
destruct p as [n m]. induction m.
- simpl. rewrite plus_0_r. destruct n; simpl; auto.
- simpl.
decide ( (n,S m) el C (n + S m) ).
+ auto.
+ eapply in_app_iff. right. right.
eapply in_filter_iff. split.
* eapply in_map_iff. exists (n, m). split. reflexivity. assert (n + S m = 1 + n + m) by lia. rewrite H. eassumption.
* rewrite Dec_reflect. eassumption.
Qed.
Lemma C_longenough n : |C n| > n.
Proof.
induction n; simpl.
- lia.
- rewrite app_length. simpl. lia.
Qed.
Definition c n : nat * nat := match elAt (C n) n with None => (0,0) | Some p => p end.
Definition c_inv p : nat := match pos p (C (eSize p)) with None => 0 | Some p => p end.
Lemma c_c_inv p : c (c_inv p) = p.
Proof.
unfold c_inv. destruct( pos p (C (eSize p)) ) eqn:A.
unfold c. destruct (elAt (C n) n ) eqn:B.
- eapply pos_elAt in A.
destruct (lt_eq_lt_dec n (eSize p)) as [[D | D] | D].
+ eapply C_ge in B. rewrite B in A. now inv A. lia.
+ subst. cut (Some p = Some p0); try congruence. now rewrite <- A, <- B.
+ eapply C_ge in A. rewrite A in B. now inv B. lia.
- eapply nth_error_none in B.
assert (|C n| > n) by eapply C_longenough. lia.
- assert (HIn : p el C (eSize p)) by eapply C_exhaustive.
eapply el_elAt in HIn. destruct HIn. eapply elAt_el in H. eapply el_pos in H. destruct H. rewrite H in *. congruence.
Qed.
Lemma c_surj : surjective c.
Proof.
eapply right_inv_surjective. unfold right_inverse. eapply c_c_inv.
Qed.
(*
Definition ESize : term := .\"p"; "p" (.\"n","m"; !Add !!(enc 1) (!Add "n" "m")).
Lemma ESize_correct p : ESize (penc p) == enc(eSize p).
Proof.
destruct p as n m. simpl.
transitivity (Add (enc 1) (Add (enc n) (enc m))). Lsimpl.
now rewrite !Add_correct.
Qed.
Definition PEq : term := .\"p1", "p2"; "p1" (.\"n1", "m1"; "p2" (.\"n2", "m2"; !Andalso (!EqN "n1" "n2") (!EqN "m1" "m2"))).
Lemma PEq_rec n1 m1 n2 m2 : PEq (penc (n1,m1)) (penc (n2,m2)) == Andalso (EqN (enc n1) (enc n2)) (EqN (enc m1) (enc m2)).
Proof.
Lsimpl.
Qed.
Lemma PEq_correct p1 p2 : PEq (penc p1) (penc p2) == true /\ p1 = p2 \/ PEq (penc p1) (penc p2) == false /\ p1 <> p2.
Proof.
destruct p1 as n1 m1, p2 as n2 m2.
destruct (EqN_correct n1 n2) as [E1 H1] | [E1 H1],
(EqN_correct m1 m2) as [E2 H2] | [E2 H2]; rewrite PEq_rec;
left; split; [Lsimpl | congruence] | right; split; [Lsimpl | congruence] .. .
Qed.
Definition CC := lam (R (.\ "C", "n"; "n" !(lenc penc (0,0)) (.\"n"; !Append ("C" "n")
(!Cons (!Pair (!Succ "n") !(enc 0))
(!Filter (.\ "x"; !Not (!(El PEq) "x" ("C" "n")))
(!Map (.\"p"; "p" (.\"n","m"; !Pair "n" (!Succ "m"))) ("C" "n")))))) 0).
Lemma CC_closed : closed CC.
Proof.
Lproc.
Qed.
Lemma CC_lam : lambda CC.
Proof.
Lproc.
Qed.
[export] Hint Resolve CC_closed CC_lam :cbv. Lemma CC_rec_0 : CC (enc 0) == lenc penc [(0,0)]. Proof. Lsimpl. Qed. Lemma CC_rec_S n : CC (enc (S n)) == Append (CC (enc n)) (Cons (Pair (Succ (enc n)) (enc 0)) (Filter (lam (Not (El PEq 0 (CC (enc n))))) (Map (lam (0 (lam(lam(Pair 1 (Succ 0)))))) (CC (enc n))))). Proof. Lsimpl. Qed. Lemma CC_correct n : CC (enc n) == lenc penc (C n). Proof with ( intros; Lproc; eauto with cbv ). induction n. - now rewrite CC_rec_0. - rewrite CC_rec_S. setoid_rewrite IHn at 1 3. rewrite Map_correct with (f := (fun p : nat * nat => let (p1,p2) := p in (p1,S p2)))... rewrite Filter_correct with (p := (fun x => not (x el C n)))... rewrite Succ_correct, Pair_correct, Cons_correct, Append_correct; try (simpl; reflexivity)... + destruct El_correct with (s := x) (A := C n) (enc := penc) (Eq := PEq) as [[H1 H2] | [H1 H2]]... * eapply PEq_correct. * right. split;[|firstorder]. transitivity (Not (((El PEq) (penc x)) (CC (enc n)))). clear IHn H1. Lsimpl. rewrite IHn,H1. apply not_rec_true. * left;split;[|firstorder]. transitivity (Not (((El PEq) (penc x)) (CC (enc n)))). clear IHn H1;Lsimpl. rewrite IHn,H1. apply not_rec_false. + split; Lproc. intros p. destruct p as [n1 m1]. clear IHn. Lsimpl. Qed. Definition Cn : term := (.\"n"; (!Nth (!CC "n") "n") !I !(penc (0,0))). Lemma Cn_closed : closed Cn. Proof. Lproc. Qed. export Hint Unfold Cn : cbv.
Hint Rewrite Cn_closed : cbv.
Lemma Cn_correct n : Cn (enc n) == penc(c n).
Proof.
transitivity (Nth (CC (enc n)) (enc n) I (penc (0,0))). Lsimpl.
rewrite CC_correct. unfold penc.
rewrite Nth_correct; Lproc.
unfold c, elAt, oenc.
destruct (nth_error (C n) n); Lsimpl.
intros; Lproc. intros; Lproc.
Qed.
*)
Import L_Notations.
Notation "A '.[' i ']'" := (elAt A i) (no associativity, at level 50).
Fixpoint appCross A B :=
match A with
| nil => nil
| a :: A => map (app a) B ++ appCross A B
end.
Fixpoint T n :=
match n with
| 0 => [#n]
| S n => let A := T n in A ++ [#(S n)] ++ filter (fun x => Dec (~ x el A)) ( map lam A ++ appCross A A )
end.
Lemma sublist_T : forall n : nat, exists (x : term) (B : list term), T (S n) = T n ++ x :: B.
Proof.
intros n. exists (# (S n)). simpl. eexists; reflexivity.
Qed.
Lemma T_S s n m : T n .[ m ] = Some s -> T (S n).[ m ] = Some s.
Proof.
destruct (sublist_T n) as [x [B H]]. rewrite H. eapply elAt_app.
Qed.
Lemma T_ge s n1 n2 m : n2 >= n1 -> T n1 .[ m ] = Some s -> T n2 .[ m ] = Some s.
Proof.
remember (S n1) as n1'. induction 1; inv Heqn1'; eauto using T_S.
Qed.
Lemma appCross_correct A B s t : (s el A /\ t el B) <-> (app s t) el appCross A B.
Proof.
split.
- induction A; simpl; intuition; subst; eauto using in_map.
- induction A; simpl; try rewrite in_app_iff in *; intros H; try tauto; destruct H as [H1 | H2]; intuition; rewrite in_map_iff in *; destruct H1; destruct H; [left|]; congruence.
Qed.
Lemma T_var n : #n el T n.
Proof.
destruct n; simpl; auto.
Qed.
Lemma T_app s t n : s el T n -> t el T n -> s t el T (S n).
Proof.
intros; simpl. decide (s t el T n); auto; simpl.
rewrite in_app_iff; simpl.
rewrite in_filter_iff, in_app_iff, <- appCross_correct.
intuition.
Qed.
Lemma T_el_ge s n m : n >= m -> s el T m -> s el T n.
Proof.
intros A B; destruct (el_elAt B); eapply elAt_el, T_ge; eassumption.
Qed.
Lemma T_lam s n : s el T n -> lam s el T (S n).
Proof.
intros; simpl; decide (lam s el T n); auto.
rewrite in_app_iff; simpl; rewrite in_filter_iff, in_app_iff, in_map_iff.
right. right. split; try left; eauto.
Qed.
Fixpoint exh_size s := match s with
| #n => n
| app s1 s2 => 1 + exh_size s1 + exh_size s2
| lam s => 1 + exh_size s
end.
Lemma T_exhaustive s : s el (T (exh_size s)).
Proof with
simpl; repeat rewrite in_app_iff; repeat rewrite in_filter_iff; try rewrite <- appCross_correct; eauto using in_filter_iff, in_app_iff, appCross_correct, el_elAt, elAt_el, T_ge, in_map.
induction s.
- destruct n; simpl; auto.
- eapply T_app; eapply T_el_ge; try eassumption; fold exh_size plus; lia.
- now eapply T_lam.
Qed.
Lemma T_longenough m : |T m| > m.
Proof.
induction m.
- simpl; lia.
- simpl. rewrite app_length. simpl. lia.
Qed.
Definition g s := match pos s (T (exh_size s)) with None => 0 | Some n => n end.
Definition g_inv n := match elAt (T n) n with None => #0 | Some n => n end.
Lemma g_inv_g s : g_inv (g s) = s.
Proof.
unfold g. destruct( pos s (T (exh_size s)) ) eqn:A.
unfold g_inv. destruct (T n .[ n ] ) eqn:B.
- eapply pos_elAt in A.
destruct (lt_eq_lt_dec n (exh_size s)) as [[D | D] | D].
+ eapply T_ge in B. rewrite B in A. now inv A. lia.
+ subst. assert (Some s = Some t) by now rewrite <- A, <- B. congruence.
+ eapply T_ge in A. rewrite A in B. now inv B. lia.
- eapply nth_error_none in B.
assert (|T n| > n) by eapply T_longenough. lia.
- assert (HIn : s el T (exh_size s)) by eapply T_exhaustive.
eapply el_elAt in HIn; eauto. destruct HIn. eapply elAt_el in H. eapply el_pos in H. destruct H. rewrite H in *; congruence.
Qed.
#[export] Hint Unfold left_inverse injective right_inverse surjective : core.
Lemma disjoint_symm X (A B : list X) : disjoint A B <-> disjoint B A.
Proof.
rewrite !disjoint_forall; firstorder.
Qed.
Lemma map_lam A : forall x, x el map lam A -> exists t, x = lam t.
Proof.
intros x B; rewrite in_map_iff in B; destruct B as [? [B _]]; subst; eauto.
Qed.
Lemma appCross_app A B : forall x, x el appCross A B -> exists s t, x = app s t.
Proof.
induction A.
- inversion 1.
- simpl; intros. rewrite in_app_iff in H. destruct H; eauto. rewrite in_map_iff in H. destruct H as [t [H1 H2]]; eauto; subst; eauto.
Qed.
Lemma T_var_not n m : m > n -> ~ #m el T n.
Proof.
induction n.
- destruct m; destruct 2; try lia. congruence. auto.
- simpl; intros A; rewrite !in_app_iff.
intros [H | H].
+ eapply IHn; now try lia.
+ destruct H as [H | H]. inv H; lia.
rewrite filter_app in H. rewrite in_app_iff in H.
destruct H as [H | H]; rewrite in_filter_iff in H; destruct H as [H1 H2].
* rewrite in_map_iff in H1. destruct H1 as [x [H1 _]]. inv H1.
* destruct (appCross_app H1) as [s [t H3]]; inv H3.
Qed.
Lemma appCross_dupfree A B : dupfree A -> dupfree B -> dupfree (appCross A B).
Proof with eauto using dupfree; intuition.
induction 1; intros dpf_B; simpl...
eapply dupfree_app...
-eapply disjoint_forall. intros y D Hy.
edestruct (appCross_app Hy) as [y1 [y2 Hyy]]; subst. eapply appCross_correct in Hy as [].
eapply in_map_iff in D. destruct D as [d [D1 D2]]. inv D1...
-eapply dupfree_map... congruence.
Qed.
Lemma dupfree_T : forall n, dupfree (T n).
Proof.
induction n.
- simpl. repeat econstructor. eauto.
- simpl. eapply dupfree_app.
+ eapply disjoint_symm, disjoint_cons. split.
* eapply T_var_not; lia.
* rewrite filter_app, disjoint_symm, disjoint_forall.
intros s A B. eapply in_app_iff in B. destruct B; eapply in_filter_iff in H;rewrite Dec_reflect in *;tauto.
+ eassumption.
+ eapply dupfreeC. rewrite in_filter_iff.
intros [A _]. rewrite in_app_iff in A. destruct A.
eapply map_lam in H. destruct H; inv H.
eapply appCross_app in H. destruct H as [s [t H]]. inv H.
eapply dupfree_filter. eapply dupfree_app.
rewrite disjoint_forall.
intros x A B. destruct (map_lam A), (appCross_app B) as [x1 [x2 B1]]. subst. inv B1.
eapply dupfree_map; congruence.
now eapply appCross_dupfree.
Qed.
Lemma T_dup n1 n2 m1 m2 x : T n1 .[m1 ] = Some x -> T n2 .[m2] = Some x -> m1 = m2.
Proof.
destruct (lt_eq_lt_dec n1 n2) as [[H | H] | H]; try subst;
try eapply lt_le_weak in H;
eauto using (T_ge), dupfree_elAt, dupfree_T.
Qed.
Lemma g_g_inv n : g(g_inv n) = n.
Proof.
unfold g_inv. destruct (T n .[ n ] ) eqn:B.
unfold g. destruct( pos t (T (exh_size t)) ) eqn:A.
- eapply pos_elAt, T_dup in A; eauto.
- assert (HIn : t el T (exh_size t)) by eapply T_exhaustive.
eapply el_elAt in HIn. destruct HIn.
eapply elAt_el in H. eapply el_pos in H. destruct H. rewrite H in A. congruence.
- eapply nth_error_none in B.
assert (|T n| > n) by eapply T_longenough.
lia.
Qed.
#[export] Hint Unfold left_inverse injective surjective g g_inv : core.
Lemma g_T : bijective g.
Proof.
split.
- eauto using left_inv_inj, g_inv_g.
- eauto using right_inv_surjective, g_g_inv.
Qed.
Fixpoint C (n : nat) :=
match n with
| 0 => [(0,0)]
| S n => C n ++ (S n, 0) :: filter (fun x => Dec (not (x el C n))) (map (fun p : nat * nat => let (p1,p2) := p in (p1,S p2)) (C n))
end.
Lemma sublist_C : forall n : nat, exists x B, C (S n) = C n ++ x :: B.
Proof.
repeat eexists.
Qed.
Lemma C_S p n m : C n .[ m ] = Some p -> C (S n).[ m ] = Some p.
Proof.
destruct (sublist_C n) as [x [B H]]. rewrite H. eapply elAt_app.
Qed.
Lemma C_ge p n1 n2 m : n2 >= n1 -> C n1 .[ m ] = Some p -> C n2 .[ m ] = Some p.
Proof.
remember (S n1) as n1'. induction 1; inv Heqn1'; eauto using C_S.
Qed.
Definition eSize (p : nat * nat) := let (n,m) := p in 1 + n + m.
Lemma C_exhaustive p : p el C( eSize p ).
Proof.
destruct p as [n m]. induction m.
- simpl. rewrite plus_0_r. destruct n; simpl; auto.
- simpl.
decide ( (n,S m) el C (n + S m) ).
+ auto.
+ eapply in_app_iff. right. right.
eapply in_filter_iff. split.
* eapply in_map_iff. exists (n, m). split. reflexivity. assert (n + S m = 1 + n + m) by lia. rewrite H. eassumption.
* rewrite Dec_reflect. eassumption.
Qed.
Lemma C_longenough n : |C n| > n.
Proof.
induction n; simpl.
- lia.
- rewrite app_length. simpl. lia.
Qed.
Definition c n : nat * nat := match elAt (C n) n with None => (0,0) | Some p => p end.
Definition c_inv p : nat := match pos p (C (eSize p)) with None => 0 | Some p => p end.
Lemma c_c_inv p : c (c_inv p) = p.
Proof.
unfold c_inv. destruct( pos p (C (eSize p)) ) eqn:A.
unfold c. destruct (elAt (C n) n ) eqn:B.
- eapply pos_elAt in A.
destruct (lt_eq_lt_dec n (eSize p)) as [[D | D] | D].
+ eapply C_ge in B. rewrite B in A. now inv A. lia.
+ subst. cut (Some p = Some p0); try congruence. now rewrite <- A, <- B.
+ eapply C_ge in A. rewrite A in B. now inv B. lia.
- eapply nth_error_none in B.
assert (|C n| > n) by eapply C_longenough. lia.
- assert (HIn : p el C (eSize p)) by eapply C_exhaustive.
eapply el_elAt in HIn. destruct HIn. eapply elAt_el in H. eapply el_pos in H. destruct H. rewrite H in *. congruence.
Qed.
Lemma c_surj : surjective c.
Proof.
eapply right_inv_surjective. unfold right_inverse. eapply c_c_inv.
Qed.
(*
Definition ESize : term := .\"p"; "p" (.\"n","m"; !Add !!(enc 1) (!Add "n" "m")).
Lemma ESize_correct p : ESize (penc p) == enc(eSize p).
Proof.
destruct p as n m. simpl.
transitivity (Add (enc 1) (Add (enc n) (enc m))). Lsimpl.
now rewrite !Add_correct.
Qed.
Definition PEq : term := .\"p1", "p2"; "p1" (.\"n1", "m1"; "p2" (.\"n2", "m2"; !Andalso (!EqN "n1" "n2") (!EqN "m1" "m2"))).
Lemma PEq_rec n1 m1 n2 m2 : PEq (penc (n1,m1)) (penc (n2,m2)) == Andalso (EqN (enc n1) (enc n2)) (EqN (enc m1) (enc m2)).
Proof.
Lsimpl.
Qed.
Lemma PEq_correct p1 p2 : PEq (penc p1) (penc p2) == true /\ p1 = p2 \/ PEq (penc p1) (penc p2) == false /\ p1 <> p2.
Proof.
destruct p1 as n1 m1, p2 as n2 m2.
destruct (EqN_correct n1 n2) as [E1 H1] | [E1 H1],
(EqN_correct m1 m2) as [E2 H2] | [E2 H2]; rewrite PEq_rec;
left; split; [Lsimpl | congruence] | right; split; [Lsimpl | congruence] .. .
Qed.
Definition CC := lam (R (.\ "C", "n"; "n" !(lenc penc (0,0)) (.\"n"; !Append ("C" "n")
(!Cons (!Pair (!Succ "n") !(enc 0))
(!Filter (.\ "x"; !Not (!(El PEq) "x" ("C" "n")))
(!Map (.\"p"; "p" (.\"n","m"; !Pair "n" (!Succ "m"))) ("C" "n")))))) 0).
Lemma CC_closed : closed CC.
Proof.
Lproc.
Qed.
Lemma CC_lam : lambda CC.
Proof.
Lproc.
Qed.
[export] Hint Resolve CC_closed CC_lam :cbv. Lemma CC_rec_0 : CC (enc 0) == lenc penc [(0,0)]. Proof. Lsimpl. Qed. Lemma CC_rec_S n : CC (enc (S n)) == Append (CC (enc n)) (Cons (Pair (Succ (enc n)) (enc 0)) (Filter (lam (Not (El PEq 0 (CC (enc n))))) (Map (lam (0 (lam(lam(Pair 1 (Succ 0)))))) (CC (enc n))))). Proof. Lsimpl. Qed. Lemma CC_correct n : CC (enc n) == lenc penc (C n). Proof with ( intros; Lproc; eauto with cbv ). induction n. - now rewrite CC_rec_0. - rewrite CC_rec_S. setoid_rewrite IHn at 1 3. rewrite Map_correct with (f := (fun p : nat * nat => let (p1,p2) := p in (p1,S p2)))... rewrite Filter_correct with (p := (fun x => not (x el C n)))... rewrite Succ_correct, Pair_correct, Cons_correct, Append_correct; try (simpl; reflexivity)... + destruct El_correct with (s := x) (A := C n) (enc := penc) (Eq := PEq) as [[H1 H2] | [H1 H2]]... * eapply PEq_correct. * right. split;[|firstorder]. transitivity (Not (((El PEq) (penc x)) (CC (enc n)))). clear IHn H1. Lsimpl. rewrite IHn,H1. apply not_rec_true. * left;split;[|firstorder]. transitivity (Not (((El PEq) (penc x)) (CC (enc n)))). clear IHn H1;Lsimpl. rewrite IHn,H1. apply not_rec_false. + split; Lproc. intros p. destruct p as [n1 m1]. clear IHn. Lsimpl. Qed. Definition Cn : term := (.\"n"; (!Nth (!CC "n") "n") !I !(penc (0,0))). Lemma Cn_closed : closed Cn. Proof. Lproc. Qed. export Hint Unfold Cn : cbv.
Hint Rewrite Cn_closed : cbv.
Lemma Cn_correct n : Cn (enc n) == penc(c n).
Proof.
transitivity (Nth (CC (enc n)) (enc n) I (penc (0,0))). Lsimpl.
rewrite CC_correct. unfold penc.
rewrite Nth_correct; Lproc.
unfold c, elAt, oenc.
destruct (nth_error (C n) n); Lsimpl.
intros; Lproc. intros; Lproc.
Qed.
*)