Commit 739c6c7a authored by charguer's avatar charguer
Browse files

demo2

parent d9a8fb78
......@@ -40,20 +40,10 @@ Tactic Notation "xassert" :=
xassert_pre ltac:(fun _ => xassert_core tt).
(********************************************************************)
(* ** Type annotations *)
let annot_let () =
let x : int = 3 in x
let annot_tuple_arg () =
(3, ([] : int list))
let annot_pattern_var x =
match (x : int list) with [] -> 1 | _ -> 0
let annot_pattern_constr () =
match ([] : int list) with [] -> 1 | _ -> 0
(********************************************************************)
......@@ -393,6 +383,99 @@ Proof using.
Qed.
(********************************************************************)
(* ** Type annotations *)
Lemma annot_let_spec :
app annot_let [tt] \[] \[= 3].
Proof using.
xcf_show.
xcf. xval. xrets~.
Qed.
Lemma annot_tuple_arg_spec :
app annot_tuple_arg [tt] \[] \[= (3, @nil int)].
Proof using.
xcf_show.
xcf. xrets~.
Qed.
Lemma annot_pattern_var_spec : forall (x:list int),
app annot_pattern_var [x] \[] \[= If x = nil then 1 else 0].
Proof using.
xcf_show.
xcf. xmatch; xrets; case_if~.
Qed.
Lemma annot_pattern_constr_spec :
app annot_pattern_constr [tt] \[] \[= 1].
Proof using.
xcf_show.
xcf. xmatch; xrets~.
Qed.
(********************************************************************)
(* ** Polymorphic functions *)
Lemma top_fun_poly_id_spec : forall A (x:A),
app top_fun_poly_id [x] \[] \[= x]. (* (fun r => \[r = x]). *)
Proof using.
xcf. xrets~.
Qed.
Lemma top_fun_poly_proj1_spec : forall A B (x:A) (y:B),
app top_fun_poly_proj1 [(x,y)] \[] \[= x].
Proof using.
xcf. xmatch. xrets~.
Qed.
Lemma top_fun_poly_proj1' : forall A B (p:A*B),
app top_fun_poly_proj1 [p] \[] \[= Datatypes.fst p].
(* TODO: maybe it's better if [fst] remains the one from Datatypes
rather than the one from Pervasives? *)
Proof using.
xcf. xmatch. xrets~.
Qed.
Lemma top_fun_poly_pair_homogeneous_spec : forall A (x y : A),
app top_fun_poly_pair_homogeneous [x y] \[] \[= (x,y)].
Proof using.
xcf. xrets~.
Qed.
(********************************************************************)
(* ** Polymorphic let bindings *)
Lemma let_poly_nil_spec : forall A,
app let_poly_nil [tt] \[] \[= @nil A].
Proof using.
xcf. dup 2.
{ xval. xrets. subst x. auto. }
{ xvals. xrets~. }
Qed.
Lemma let_poly_nil_pair_spec : forall A B,
app let_poly_nil_pair [tt] \[] \[= (@nil A, @nil B)].
Proof using.
xcf. xvals. xrets~.
Qed.
Lemma let_poly_nil_pair_homogeneous_spec : forall A,
app let_poly_nil_pair_homogeneous [tt] \[] \[= (@nil A, @nil A)].
Proof using.
xcf. xvals. xrets~.
Qed.
Lemma let_poly_nil_pair_heterogeneous_spec : forall A,
app let_poly_nil_pair_heterogeneous [tt] \[] \[= (@nil A, @nil int)].
Proof using.
xcf. xvals. xrets~.
Qed.
(********************************************************************)
......@@ -472,63 +555,6 @@ Qed.
(********************************************************************)
(* ** Polymorphic functions *)
Lemma top_fun_poly_id : forall A (x:A),
app top_fun_poly_id [x] \[] \[= x]. (* (fun r => \[r = x]). *)
Proof using.
xcf.
Qed.
Lemma top_fun_poly_proj1 : forall A B (x:A) (y:B),
app top_fun_poly_proj1 [(x,y)] \[] \[= x]
Proof using.
xcf.
Qed.
Lemma top_fun_poly_proj1' : forall A B (p:A*B),
app top_fun_poly_proj1 [p] \[] \[= fst x]. (* (fun r => \[r = fst x]). *)
Proof using.
xcf.
Qed.
Lemma top_fun_poly_pair_homogeneous : forall A (x y : A),
app top_fun_poly_pair_homogeneous [x y] \[] \[= (x,y)].
Proof using.
xcf.
Qed.
(********************************************************************)
(* ** Polymorphic let bindings *)
Lemma let_poly_nil () =
let x = [] in x
Proof using.
xcf.
Qed.
Lemma let_poly_nil_pair () =
let x = ([], []) in x
Proof using.
xcf.
Qed.
Lemma let_poly_nil_pair_homogeneous () =
let x : ('a list * 'a list) = ([], []) in x
Proof using.
xcf.
Qed.
Lemma let_poly_nil_pair_heterogeneous () =
let x : ('a list * int list) = ([], []) in x
Proof using.
xcf.
Qed.
*)
......
......@@ -1380,8 +1380,13 @@ Tactic Notation "xseq" "*" constr(H) := xseq H; xauto*.
*)
Ltac xval_pre tt :=
xextract_check_not_needed tt;
xuntag tag_val;
apply local_erase.
Ltac xval_impl x Hx :=
apply local_erase; intros x Hx.
xval_pre tt; intros x Hx.
Tactic Notation "xval" "as" simple_intropattern(x) simple_intropattern(Hx) :=
xval_impl x Hx.
......@@ -1390,7 +1395,7 @@ Tactic Notation "xval" "as" simple_intropattern(x) :=
let Hx := fresh "P" x in xval_impl x Hx.
Ltac xval_anonymous_impl tt :=
apply local_erase; intro; let x := get_last_hyp tt in revert x;
xval_pre tt; intro; let x := get_last_hyp tt in revert x;
let Hx := fresh "P" x in intros x Hx.
Tactic Notation "xval" :=
......@@ -1400,7 +1405,7 @@ Tactic Notation "xval" :=
the equality [x = v] produced by [xval]. *)
Ltac xvals_impl tt :=
apply local_erase; intro; intro_subst.
xval_pre tt; intro; intro_subst.
Tactic Notation "xvals" :=
xvals_impl tt.
......@@ -1418,7 +1423,7 @@ Ltac xval_st_core P x Hx :=
let E := fresh in intros x E; asserts Hx: (P x); [ subst x | clear E ].
Ltac xval_st_impl P x Hx :=
apply local_erase; xval_st_core P x Hx.
xval_pre tt; xval_st_core P x Hx.
Tactic Notation "xval_st" constr(P) "as" simple_intropattern(x) simple_intropattern(Hx) :=
xval_st_impl P x Hx.
......@@ -1427,7 +1432,7 @@ Tactic Notation "xval_st" constr(P) "as" simple_intropattern(x) :=
let Hx := fresh "P" x in xval_st_impl P x Hx.
Ltac xval_st_anonymous_impl P :=
apply local_erase; intro; let x := get_last_hyp tt in revert x;
xval_pre tt; intro; let x := get_last_hyp tt in revert x;
let Hx := fresh "P" x in xval_st_core P x Hx.
Tactic Notation "xval_st" constr(P) :=
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment