Lists
Require Import internalize_tac crush_no_refl_ideas LBool LOptions LNat Base SumBool.
Require Export List.
Section Fix_X.
Variable (X:Set).
Variable (intX : registered X) .
Fixpoint list_enc (A : list X) :=
match A with
| nil => lam (lam #1)
| cons a A => lam(lam (#0 (enc a) (list_enc A)))
end.
(* do not use this, but (internalizes _) once registered!*)
Definition lists_cons : term := Eval cbv in .\"a", "A", "n", "c"; "c" "a" "A".
(*instance contains proc-ness and injectivity of encoding*)
Global Instance register_list : registered (list X).
Proof.
register list_enc.
Defined.
Global Instance list_enc_inj (H : inj_reg intX) : inj_reg register_list.
Proof.
register_inj.
Defined.
(* now we must register the constructors*)
Global Instance term_nil : internalized (@nil X).
Proof.
internalizeC (list_enc nil).
Defined.
Global Instance term_cons : internalized (@cons X).
Proof.
internalizeC lists_cons.
Defined.
Lemma list_enc_correct (A:list X) (s t:term): proc s -> proc t -> enc A s t >* match A with nil => s | cons a A' => t (enc a) (enc (A')) end.
Proof.
enc_correct.
Qed.
Hint Extern 0 (Lvw.app (Lvw.app (@enc (@list X) _ _) _) _ >* _)=> apply list_enc_correct;value : LCor.
Global Instance term_append : internalized (@List.app X).
Proof.
internalizeR. induction y; recStep P; crush.
Defined.
Global Instance term_filter: internalized (@Base.filter X).
Proof.
internalize. do 2 redStep. recRem. cbn in R0. hnf in R0. induction y1;recStep P;crush.
decide (y a);destruct (y0 a);try tauto; crush.
Defined.
Global Instance term_nth : internalized (@nth X).
Proof.
internalizeR. revert y. induction y0; destruct y; recStep P;crush.
Defined.
Fixpoint inb (H : eq_dec X) (x:X) A :=
match A with
nil => false
| a::A' => if (decision (a=x)) then true else inb H x A'
end.
Lemma inb_spec : forall H x A, Bool.reflect (In x A) (inb H x A).
Proof.
intros H x A. induction A.
-constructor. tauto.
-simpl. decide (a=x).
+constructor. tauto.
+inv IHA. destruct (inb H x A).
*constructor. tauto.
*constructor. tauto.
*constructor. tauto.
Defined.
Local Instance term_inb : internalized inb.
Proof.
internalizeR. induction y1;recStep P;crush.
dec;destruct y;try tauto; crush.
Defined.
Global Instance term_list_in_dec: internalized (list_in_dec (X:=X)).
Proof.
pose (s := fun x y H => to_sumbool (inb H x y)).
internalizeWith s.
apply reflect_dec.
apply inb_spec.
Defined.
Global Instance term_pos: internalized (@pos X).
Proof.
internalize. redStep. recRem. induction y1;recStep P;crush. unfold decision.
destruct y;crush. destruct pos;crush.
Defined.
End Fix_X.
Hint Extern 0 (Lvw.app (Lvw.app (@enc (@list _) _ _) _) _ >* _)=> apply list_enc_correct;value : LCor.
Instance term_map (X Y:Set) (Hx : registered X) (Hy:registered Y): internalized (@map X Y).
Proof.
internalize. redStep. recRem. induction y0; recStep P;crush.
Defined.
Instance term_nth_error (X:Set) (Hx : registered X): internalized (@nth_error X).
Proof.
pose (f A n := nth n (map (@Some X) A) None).
assert (forall A n, f A n = nth_error A n).
{ induction A.
-destruct n; reflexivity.
-destruct n. reflexivity. simpl. rewrite <- IHA. reflexivity.
}
internalizeWith f. reflexivity. value. rewrite <- H at 1. reflexivity.
Defined.
Instance term_elAt (X:Set) (Hx : registered X) : internalized (@elAt X).
Proof.
apply term_nth_error.
Defined.
Require Export List.
Section Fix_X.
Variable (X:Set).
Variable (intX : registered X) .
Fixpoint list_enc (A : list X) :=
match A with
| nil => lam (lam #1)
| cons a A => lam(lam (#0 (enc a) (list_enc A)))
end.
(* do not use this, but (internalizes _) once registered!*)
Definition lists_cons : term := Eval cbv in .\"a", "A", "n", "c"; "c" "a" "A".
(*instance contains proc-ness and injectivity of encoding*)
Global Instance register_list : registered (list X).
Proof.
register list_enc.
Defined.
Global Instance list_enc_inj (H : inj_reg intX) : inj_reg register_list.
Proof.
register_inj.
Defined.
(* now we must register the constructors*)
Global Instance term_nil : internalized (@nil X).
Proof.
internalizeC (list_enc nil).
Defined.
Global Instance term_cons : internalized (@cons X).
Proof.
internalizeC lists_cons.
Defined.
Lemma list_enc_correct (A:list X) (s t:term): proc s -> proc t -> enc A s t >* match A with nil => s | cons a A' => t (enc a) (enc (A')) end.
Proof.
enc_correct.
Qed.
Hint Extern 0 (Lvw.app (Lvw.app (@enc (@list X) _ _) _) _ >* _)=> apply list_enc_correct;value : LCor.
Global Instance term_append : internalized (@List.app X).
Proof.
internalizeR. induction y; recStep P; crush.
Defined.
Global Instance term_filter: internalized (@Base.filter X).
Proof.
internalize. do 2 redStep. recRem. cbn in R0. hnf in R0. induction y1;recStep P;crush.
decide (y a);destruct (y0 a);try tauto; crush.
Defined.
Global Instance term_nth : internalized (@nth X).
Proof.
internalizeR. revert y. induction y0; destruct y; recStep P;crush.
Defined.
Fixpoint inb (H : eq_dec X) (x:X) A :=
match A with
nil => false
| a::A' => if (decision (a=x)) then true else inb H x A'
end.
Lemma inb_spec : forall H x A, Bool.reflect (In x A) (inb H x A).
Proof.
intros H x A. induction A.
-constructor. tauto.
-simpl. decide (a=x).
+constructor. tauto.
+inv IHA. destruct (inb H x A).
*constructor. tauto.
*constructor. tauto.
*constructor. tauto.
Defined.
Local Instance term_inb : internalized inb.
Proof.
internalizeR. induction y1;recStep P;crush.
dec;destruct y;try tauto; crush.
Defined.
Global Instance term_list_in_dec: internalized (list_in_dec (X:=X)).
Proof.
pose (s := fun x y H => to_sumbool (inb H x y)).
internalizeWith s.
apply reflect_dec.
apply inb_spec.
Defined.
Global Instance term_pos: internalized (@pos X).
Proof.
internalize. redStep. recRem. induction y1;recStep P;crush. unfold decision.
destruct y;crush. destruct pos;crush.
Defined.
End Fix_X.
Hint Extern 0 (Lvw.app (Lvw.app (@enc (@list _) _ _) _) _ >* _)=> apply list_enc_correct;value : LCor.
Instance term_map (X Y:Set) (Hx : registered X) (Hy:registered Y): internalized (@map X Y).
Proof.
internalize. redStep. recRem. induction y0; recStep P;crush.
Defined.
Instance term_nth_error (X:Set) (Hx : registered X): internalized (@nth_error X).
Proof.
pose (f A n := nth n (map (@Some X) A) None).
assert (forall A n, f A n = nth_error A n).
{ induction A.
-destruct n; reflexivity.
-destruct n. reflexivity. simpl. rewrite <- IHA. reflexivity.
}
internalizeWith f. reflexivity. value. rewrite <- H at 1. reflexivity.
Defined.
Instance term_elAt (X:Set) (Hx : registered X) : internalized (@elAt X).
Proof.
apply term_nth_error.
Defined.