Library Lists
Require Export Bool Options.
Section Fix_X.
Variable X : Type.
Variable enc : X -> term.
Hypothesis enc_lam : (forall x, lambda (enc x)).
Hypothesis enc_cls : (forall x, closed (enc x)).
Hint Resolve enc_lam enc_cls : cbv.
Hint Rewrite enc_cls : cbv.
Fixpoint lenc (A : list X) :=
match A with
| nil => lam (lam #1)
| a::A => lam(lam (#0 (enc a) (lenc A)))
end.
Definition Nil : term := .\ "n", "c"; "n".
Definition Cons: term := .\ "a", "A", "n", "c"; "c" "a" "A".
Hint Unfold Nil Cons : cbv.
Lemma lenc_cls A : closed (lenc A).
Proof.
induction A.
- value.
- intros ? ? ; simpl; now rewrite IHA, enc_cls.
Qed.
Lemma lenc_lam A : lambda (lenc A).
Proof.
destruct A; value.
Qed.
Hint Resolve lenc_cls lenc_lam : cbv.
Hint Rewrite lenc_cls : cbv.
Lemma Cons_correct a A : Cons (enc a) (lenc A) == lenc(a::A).
Proof.
crush.
Qed.
Definition Append := R (.\ "app", "A", "B";
"A" "B" (.\"a", "A"; !Cons "a" ("app" "A" "B"))).
Hint Unfold Append : cbv.
Lemma Append_rec_Nil B : Append Nil (lenc B) == (lenc B).
Proof.
crush.
Qed.
Lemma Append_rec_Cons a A B : Append (lenc (a::A)) (lenc B) == Cons (enc a) ((lam (Append #0)) (lenc A) (lenc B)).
Proof.
crush.
Qed.
Lemma Append_correct A B : Append (lenc A) (lenc B) == lenc(A ++ B).
Proof.
induction A.
- eapply Append_rec_Nil.
- rewrite Append_rec_Cons.
now rewrite !Eta, IHA, Cons_correct; value.
Qed.
Definition sim (F : term) f := proc F /\ forall x, F (enc x) == (enc (f x)).
Definition Map := R (.\ "map", "F", "A";
"A" !Nil (.\"a", "A"; !Cons ("F" "a") ("map" "F" "A"))).
Lemma Map_rec_Nil F : proc F -> Map F Nil == Nil.
Proof.
intros [? ?]; crush.
Qed.
Lemma Map_rec_Cons a A F : proc F ->
Map F (lenc (a::A)) == Cons (F (enc a)) ((lam (Map #0)) F (lenc A)).
Proof.
intros [? ?]; crush.
Qed.
Lemma Map_correct f A F : sim F f ->
Map F (lenc A) == lenc(map f A).
Proof.
intros [[? ?] ?].
induction A.
- eapply Map_rec_Nil; eauto.
- rewrite Map_rec_Cons; eauto.
now rewrite !Eta, H1, IHA, Cons_correct; value.
Qed.
Variable Eq : term.
Hypothesis Eq_correct: forall s t : X,
(Eq (enc s) (enc t) == true /\ s = t) \/ (Eq (enc s) (enc t) == false /\ s <> t).
Hypothesis Eq_cls : closed Eq.
Hint Resolve Eq_cls.
Hint Rewrite Eq_cls.
Definition El := R (.\ "El", "x", "A";
"A" !false (.\"a", "A"; !Orelse (!Eq "a" "x") ("El" "x" "A"))).
Hint Unfold El : cbv.
Lemma El_nil s : El (enc s) Nil == false.
Proof.
crush.
Qed.
Lemma El_Cons s a A : El (enc s) (lenc (a :: A)) == Orelse (Eq (enc a) (enc s)) ((lam (El #0)) (enc s) (lenc A)).
Proof.
crush.
Qed.
Lemma El_correct s A : (El (enc s) (lenc A) == true /\ s el A) \/ (El (enc s) (lenc A) == false /\ ~ s el A).
Proof.
induction A.
- eauto using El_nil.
- destruct (Eq_correct a s) as [[HE E] | [HE N]].
+ subst. left. split; auto. rewrite El_Cons, HE, !Eta; value. destruct IHA as [[H _] | [H _]]; rewrite H; eauto using Orelse_rec_tt, Orelse_rec_tf; auto.
+ destruct IHA as [[H I] | [H I]].
* left. split; auto.
rewrite El_Cons, HE, !Eta, H; value. eapply Orelse_rec_ft.
* right. split; auto.
rewrite El_Cons, HE, !Eta, H; value. eapply Orelse_rec_ff.
firstorder.
Qed.
Definition Filter := R (.\ "F", "p", "A";
"A" !Nil (.\"a", "A"; ("p" "a") (!Cons "a" ("F" "p" "A")) ("F" "p" "A"))).
Hint Unfold Filter : cbv.
Lemma Filter_Nil P : proc P -> Filter P Nil == Nil.
Proof.
destruct 1; crush.
Qed.
Lemma proc_lambda p : proc p -> lambda p.
Proof.
firstorder intuition.
Qed.
Hint Resolve proc_lambda : cbv.
Lemma Filter_Cons (P : term) a A :
proc P ->
Filter P (lenc (a::A))
== (P (enc a)) (Cons (enc a) ((lam (Filter #0)) P (lenc A))) ((lam (Filter #0)) P (lenc A)).
Proof.
intros. crush.
Qed.
Lemma Filter_correct (P : term) p A (D : (forall x : X, dec (p x))) :
proc P ->
(forall x, P (enc x) == true /\ p x \/ P (enc x) == false /\ ~ p x)
-> Filter P (lenc A) == lenc(@filter X p D A).
Proof with eauto.
intros proc_P dec_P.
induction A.
- now rewrite Filter_Nil.
- rewrite Filter_Cons... destruct (dec_P a) as [[HP Hp] | [HP Hp]];
simpl; decide (p a); try tauto;
rewrite !Eta; value;
rewrite HP, IHA, Cons_correct;
crush.
Qed.
Definition Nth := R (.\ "nth", "A", "n";
"n" ("A" !none (.\ "a", "A"; !some "a"))
(.\"n"; ("A" !none (.\"a", "A"; "nth" "A" "n"))) ).
Lemma Nth_Nil n : Nth Nil (Nat.enc n) == none.
Proof.
destruct n; crush.
Qed.
Lemma Nth_0 a A : Nth (lenc(a::A)) Zero == some (enc a).
Proof.
transitivity ((λ (λ #1 (enc a)))). crush.
symmetry. crush.
Qed.
Lemma Nth_Sn a A n : Nth (lenc(a::A)) (Nat.enc(S n)) == (lam (Nth #0)) (lenc A) (Nat.enc n).
Proof.
crush.
Qed.
Definition oenc x := match x with None => none | Some x => (lam(lam(#1 (enc x)))) end.
Lemma Nth_correct A n : Nth (lenc A) (Nat.enc n) == oenc(nth_error A n).
Proof.
revert A; induction n; intros A.
- destruct A.
+ now rewrite Nth_Nil.
+ rewrite Nth_0; crush.
- destruct A.
+ now rewrite Nth_Nil.
+ rewrite Nth_Sn.
now rewrite !Eta, IHn; value.
Qed.
Definition Pos := R (.\ "pos", "s", "A";
"A" !none (.\ "a", "A"; !Eq "s" "a" !(lam (some Zero))
(.\""; "pos" "s" "A" (.\"n"; !some (!Succ "n")) !none) !I)).
Lemma Pos_rec_nil s : Pos (enc s) Nil == none.
Proof.
crush.
Qed.
Lemma Pos_rec_cons s a A : Pos (enc s) (lenc(a::A)) ==
Eq (enc s) (enc a) (lam(some Zero)) (lam ( (lam(Pos #0)) (enc s) (lenc A) (lam(some (Succ #0))) none)) I.
Proof.
crush.
Qed.
Lemma Pos_correct s A (E : eq_dec X) : Pos (enc s) (lenc A) == match pos s A with None => none | Some n => some (Nat.enc n) end.
Proof.
induction A.
- now rewrite Pos_rec_nil.
- rewrite Pos_rec_cons. simpl. destruct (Eq_correct s a) as [[F B] | [F B]].
+ rewrite F. decide (s = a); try tauto. crush.
+ rewrite F. decide (s = a); try tauto; destruct (pos s A); crush.
Qed.
End Fix_X.
Section Fix_X.
Variable X : Type.
Variable enc : X -> term.
Hypothesis enc_lam : (forall x, lambda (enc x)).
Hypothesis enc_cls : (forall x, closed (enc x)).
Hint Resolve enc_lam enc_cls : cbv.
Hint Rewrite enc_cls : cbv.
Fixpoint lenc (A : list X) :=
match A with
| nil => lam (lam #1)
| a::A => lam(lam (#0 (enc a) (lenc A)))
end.
Definition Nil : term := .\ "n", "c"; "n".
Definition Cons: term := .\ "a", "A", "n", "c"; "c" "a" "A".
Hint Unfold Nil Cons : cbv.
Lemma lenc_cls A : closed (lenc A).
Proof.
induction A.
- value.
- intros ? ? ; simpl; now rewrite IHA, enc_cls.
Qed.
Lemma lenc_lam A : lambda (lenc A).
Proof.
destruct A; value.
Qed.
Hint Resolve lenc_cls lenc_lam : cbv.
Hint Rewrite lenc_cls : cbv.
Lemma Cons_correct a A : Cons (enc a) (lenc A) == lenc(a::A).
Proof.
crush.
Qed.
Definition Append := R (.\ "app", "A", "B";
"A" "B" (.\"a", "A"; !Cons "a" ("app" "A" "B"))).
Hint Unfold Append : cbv.
Lemma Append_rec_Nil B : Append Nil (lenc B) == (lenc B).
Proof.
crush.
Qed.
Lemma Append_rec_Cons a A B : Append (lenc (a::A)) (lenc B) == Cons (enc a) ((lam (Append #0)) (lenc A) (lenc B)).
Proof.
crush.
Qed.
Lemma Append_correct A B : Append (lenc A) (lenc B) == lenc(A ++ B).
Proof.
induction A.
- eapply Append_rec_Nil.
- rewrite Append_rec_Cons.
now rewrite !Eta, IHA, Cons_correct; value.
Qed.
Definition sim (F : term) f := proc F /\ forall x, F (enc x) == (enc (f x)).
Definition Map := R (.\ "map", "F", "A";
"A" !Nil (.\"a", "A"; !Cons ("F" "a") ("map" "F" "A"))).
Lemma Map_rec_Nil F : proc F -> Map F Nil == Nil.
Proof.
intros [? ?]; crush.
Qed.
Lemma Map_rec_Cons a A F : proc F ->
Map F (lenc (a::A)) == Cons (F (enc a)) ((lam (Map #0)) F (lenc A)).
Proof.
intros [? ?]; crush.
Qed.
Lemma Map_correct f A F : sim F f ->
Map F (lenc A) == lenc(map f A).
Proof.
intros [[? ?] ?].
induction A.
- eapply Map_rec_Nil; eauto.
- rewrite Map_rec_Cons; eauto.
now rewrite !Eta, H1, IHA, Cons_correct; value.
Qed.
Variable Eq : term.
Hypothesis Eq_correct: forall s t : X,
(Eq (enc s) (enc t) == true /\ s = t) \/ (Eq (enc s) (enc t) == false /\ s <> t).
Hypothesis Eq_cls : closed Eq.
Hint Resolve Eq_cls.
Hint Rewrite Eq_cls.
Definition El := R (.\ "El", "x", "A";
"A" !false (.\"a", "A"; !Orelse (!Eq "a" "x") ("El" "x" "A"))).
Hint Unfold El : cbv.
Lemma El_nil s : El (enc s) Nil == false.
Proof.
crush.
Qed.
Lemma El_Cons s a A : El (enc s) (lenc (a :: A)) == Orelse (Eq (enc a) (enc s)) ((lam (El #0)) (enc s) (lenc A)).
Proof.
crush.
Qed.
Lemma El_correct s A : (El (enc s) (lenc A) == true /\ s el A) \/ (El (enc s) (lenc A) == false /\ ~ s el A).
Proof.
induction A.
- eauto using El_nil.
- destruct (Eq_correct a s) as [[HE E] | [HE N]].
+ subst. left. split; auto. rewrite El_Cons, HE, !Eta; value. destruct IHA as [[H _] | [H _]]; rewrite H; eauto using Orelse_rec_tt, Orelse_rec_tf; auto.
+ destruct IHA as [[H I] | [H I]].
* left. split; auto.
rewrite El_Cons, HE, !Eta, H; value. eapply Orelse_rec_ft.
* right. split; auto.
rewrite El_Cons, HE, !Eta, H; value. eapply Orelse_rec_ff.
firstorder.
Qed.
Definition Filter := R (.\ "F", "p", "A";
"A" !Nil (.\"a", "A"; ("p" "a") (!Cons "a" ("F" "p" "A")) ("F" "p" "A"))).
Hint Unfold Filter : cbv.
Lemma Filter_Nil P : proc P -> Filter P Nil == Nil.
Proof.
destruct 1; crush.
Qed.
Lemma proc_lambda p : proc p -> lambda p.
Proof.
firstorder intuition.
Qed.
Hint Resolve proc_lambda : cbv.
Lemma Filter_Cons (P : term) a A :
proc P ->
Filter P (lenc (a::A))
== (P (enc a)) (Cons (enc a) ((lam (Filter #0)) P (lenc A))) ((lam (Filter #0)) P (lenc A)).
Proof.
intros. crush.
Qed.
Lemma Filter_correct (P : term) p A (D : (forall x : X, dec (p x))) :
proc P ->
(forall x, P (enc x) == true /\ p x \/ P (enc x) == false /\ ~ p x)
-> Filter P (lenc A) == lenc(@filter X p D A).
Proof with eauto.
intros proc_P dec_P.
induction A.
- now rewrite Filter_Nil.
- rewrite Filter_Cons... destruct (dec_P a) as [[HP Hp] | [HP Hp]];
simpl; decide (p a); try tauto;
rewrite !Eta; value;
rewrite HP, IHA, Cons_correct;
crush.
Qed.
Definition Nth := R (.\ "nth", "A", "n";
"n" ("A" !none (.\ "a", "A"; !some "a"))
(.\"n"; ("A" !none (.\"a", "A"; "nth" "A" "n"))) ).
Lemma Nth_Nil n : Nth Nil (Nat.enc n) == none.
Proof.
destruct n; crush.
Qed.
Lemma Nth_0 a A : Nth (lenc(a::A)) Zero == some (enc a).
Proof.
transitivity ((λ (λ #1 (enc a)))). crush.
symmetry. crush.
Qed.
Lemma Nth_Sn a A n : Nth (lenc(a::A)) (Nat.enc(S n)) == (lam (Nth #0)) (lenc A) (Nat.enc n).
Proof.
crush.
Qed.
Definition oenc x := match x with None => none | Some x => (lam(lam(#1 (enc x)))) end.
Lemma Nth_correct A n : Nth (lenc A) (Nat.enc n) == oenc(nth_error A n).
Proof.
revert A; induction n; intros A.
- destruct A.
+ now rewrite Nth_Nil.
+ rewrite Nth_0; crush.
- destruct A.
+ now rewrite Nth_Nil.
+ rewrite Nth_Sn.
now rewrite !Eta, IHn; value.
Qed.
Definition Pos := R (.\ "pos", "s", "A";
"A" !none (.\ "a", "A"; !Eq "s" "a" !(lam (some Zero))
(.\""; "pos" "s" "A" (.\"n"; !some (!Succ "n")) !none) !I)).
Lemma Pos_rec_nil s : Pos (enc s) Nil == none.
Proof.
crush.
Qed.
Lemma Pos_rec_cons s a A : Pos (enc s) (lenc(a::A)) ==
Eq (enc s) (enc a) (lam(some Zero)) (lam ( (lam(Pos #0)) (enc s) (lenc A) (lam(some (Succ #0))) none)) I.
Proof.
crush.
Qed.
Lemma Pos_correct s A (E : eq_dec X) : Pos (enc s) (lenc A) == match pos s A with None => none | Some n => some (Nat.enc n) end.
Proof.
induction A.
- now rewrite Pos_rec_nil.
- rewrite Pos_rec_cons. simpl. destruct (Eq_correct s a) as [[F B] | [F B]].
+ rewrite F. decide (s = a); try tauto. crush.
+ rewrite F. decide (s = a); try tauto; destruct (pos s A); crush.
Qed.
End Fix_X.