Skip to content

GitLab

Commit 78e95944 authored by charguer's avatar charguer
Browse files

tlc migration and polymorphic_eq

parent f385602f
Hide whitespace changes
Inline Side-by-side
TODO
View file @ 78e95944
- rename xuntag_goal
- generate instance of comparable
(* DO not use; only used during the normalization phase *)
external ( & ) : bool -> bool -> bool = "%sequand"
external ( or ) : bool -> bool -> bool = "%sequor"
......@@ -16,6 +23,10 @@ external ( or ) : bool -> bool -> bool = "%sequor"
- xlet Q => xif Q mais avec branche
- hint spec based on type args
MAJOR TODAY
......@@ -31,8 +42,23 @@ MAJOR NEXT
- patterns and when clauses
- add support for pure records
Record 'A T := T_intro { f' : T1; .. }
if mutually recursive, encode record def using
Ind 'A T := T_intro : T1 -> ... -> 'A T
Implicit Types T ['A]
Def f' 'A (p:'A T) :=
match p with T_intro x1 .. xN => xi end
alloc: (T_intro v1 .. vN : typ)
set : impossible
with : match r with T_intro x1 .. xN => T_intro x1 .. yI .. xN
=> requires the order of labels to be fixed as in the definition.
- record with
- record with imperative
- partial/over application
......@@ -42,12 +68,16 @@ MAJOR NEXT
MAJOR NEXT NEXT
- xwhile: error reporting when arguments don't have the right types.
- eliminate notations for tags
- record single field and array single cell notation
Notation "x `. f '~>' S" :=
Notation "x `[ i ] '~>' S" :=
Notation "x `[ i ] '~>' S" :=
t ~> Array L= t ~> Arraylen n * exists G, Groupof Cell G
dom G = [0,n] * lenght L = n * forall i indom G, L[i] = G[i]
- realize array specification using single-cell array specifications
......@@ -56,6 +86,8 @@ MAJOR NEXT NEXT
- mutually recursive polymorhpic functions have too many type variables
quantified: we need one set of fvs for each def in the recursion.
MAJOR POSTPONED
- support char
......@@ -135,3 +167,16 @@ MAKEFILE BEAUTIFY
During the proof, the user needs to provide the proposition
[P] that is tested by the assertion. This proposition can
be assumed to be true after the assert is executed.
##################################################################
# COQ BUG
-async-proofs off
-async-proofs-j n
for coqide is not documented
omega requires Z.sub to be transparent, but this is an issue for simpl.
examples/BasicDemos/Demo_proof.v
View file @ 78e95944
......@@ -337,13 +337,17 @@ Proof using. xcf*. Qed.
Lemma ret_unit_spec :
app ret_unit [tt] \[] \[= tt]. (* (fun (_:unit) => \[]).*) (* same as (# \[]). *)
Proof using.
xcf. dup 5. (* TODO : accolade *)
xret. xsimpl. auto.
(* demos *)
xrets. auto.
xrets*.
xret_no_gc. xsimpl. auto.
xret_no_clean. xsimpl*.
xcf. dup 8.
{ xret. xsimpl. auto. }
{ xrets. auto. }
{ xrets*. }
{ xret_no_gc. xsimpl. auto. }
{ xret_no_clean. xsimpl*. } (* differs only on nontrivial goals *)
{ xret_no_pull. xsimpl*. } (* differs only on a let binding *)
{ try xret (fun r => \[r = tt /\ True]).
xpost. xret (fun r => \[r = tt /\ True]). xsimpl. auto. xsimpl. auto. }
{ try xrets (fun r => \[r = tt /\ True]).
xpost. xrets (fun r => \[r = tt /\ True]). auto. xsimpl. auto. }
Qed.
Lemma ret_int_spec :
......@@ -427,7 +431,7 @@ Lemma let_fun_const_spec :
app let_fun_const [tt] \[] \[= 3].
Proof using.
xcf. dup 10.
{ xfun. apply Sf. xtag_goal. xrets~. }
{ xfun. apply Sf. xtag_pre_post. xrets~. }
{ xfun as g. apply Sg. skip. }
{ xfun as g. xapp. xret. skip. }
{ xfun as g G. apply G. skip. }
......@@ -493,7 +497,7 @@ Lemma let_fun_in_let_spec :
(fun g => \[ forall A (x:A), app g [x] \[] \[= x] ]).
Proof using.
xcf. xlet (fun g => \[ forall A (x:A), app g [x] \[] \[= x] ]).
(* TODO: could we get away by typing just [xlet] above? *)
(* TODO: use [xpush] *)
{ xassert. { xret. }
xfun. xrets. =>>. xapp. xrets~. }
{ =>> M. xrets~. }
......@@ -629,10 +633,14 @@ Lemma compare_poly_spec :
app compare_poly [tt] \[] \[= tt].
Proof using.
xcf.
xlet_poly_keep (= true). { xapps. typeclass. xsimpl. subst r. logics~. } intro_subst.
xapp. typeclass. intro_subst.
xlet_poly_keep (= true). { xapps. typeclass. xsimpl. subst r. logics~. } intro_subst.
xapp. typeclass. intro_subst.
xlet_poly_keep (= true).
{ xapps. xpolymorphic_eq. xsimpl. subst r. logics~. }
intro_subst.
xapp. xpolymorphic_eq. intro_subst.
xlet_poly_keep (= true).
{ xapps. xpolymorphic_eq. xsimpl. subst r. logics~. }
intro_subst.
xapp. xpolymorphic_eq. intro_subst.
xrets~.
Qed.
......@@ -668,7 +676,7 @@ Proof using.
app f [k v l] \[] \[= list_update k v l ]).
{ xmatch.
{ xrets~. }
{ xapps~. xret. xpulls. xif.
{ xapps~. xrets. xif.
{ xrets. case_if. auto. }
{ xapp_spec infix_emark_eq_gen_spec. intros M. xif.
{ xrets. case_if~. }
......@@ -906,6 +914,27 @@ Qed.
(********************************************************************)
(* ** While loops *)
(* TODO: fix hack *)
Definition Zsub := Zminus.
Infix "-" := Zsub : Int_scope.
Open Scope Int_scope.
Lemma Zsub_eq : Zsub = Zminus.
Proof using. auto. Qed.
Opaque Zsub.
Hint Rewrite Zsub_eq : rew_maths.
(* end hack *)
(* TODO: move *)
Hint Rewrite downto_def nat_upto_wf upto_def : rew_maths.
Lemma while_decr_spec :
app while_decr [tt] \[] \[= 3].
Proof using.
......@@ -918,8 +947,8 @@ Proof using.
applys (rm HR). xlet.
{ xapps. xrets. }
{ xpulls. xif.
{ xseq. xapps. xapps. simpl. xapplys IH. hnf. skip. skip. skip. } (* TODO math. *)
{ xrets. math. skip. } } (* TODO math. *)
{ xseq. xapps. xapps. simpl. xapplys IH. math. math. math. }
{ xrets. math. math. } }
xapps. xsimpl~. }
{ xwhile as R. skip. skip. }
{ xwhile_inv (fun b k => \[k >= 0] \* \[b = isTrue (k > 0)]
......@@ -929,15 +958,15 @@ Proof using.
{ xapps. xrets. }
{ xpulls. xif.
{ xseq. xapps. xapps. simpl. xapplys FS.
hnf. skip. skip. eauto. skip. eauto. eauto. } (* TODO math. *)
hnf. math. math. eauto. math. eauto. eauto. }
{ xret. xsimpl. math. math. } } }
{ intros. xapps. xsimpl. skip. (* math. *) } }
{ intros. xapps. xsimpl. math. } }
{ xwhile_inv_basic (fun b k => \[k >= 0] \* \[b = isTrue (k > 0)]
\* n ~~> k \* c ~~> (3-k)) (downto 0).
{ xsimpl*. math. }
{ intros b k. xpull ;=> Hk Hb. xapps. xrets. xauto*. math. }
{ intros k. xpull ;=> Hk Hb. xapps. xapps. xsimpl. skip. eauto. skip. hnf. skip. }
{ => k Hk Hb. xapp. xsimpl. skip. (* math.*) } }
{ intros k. xpull ;=> Hk Hb. xapps. xapps. xsimpl. math. eauto. math. math. }
{ => k Hk Hb. xapp. xsimpl. math. } }
{ (* using a measure [fun k => abs k] *)
xwhile_inv_basic (fun b k => \[k >= 0] \* \[b = isTrue (k > 0)]
\* n ~~> k \* c ~~> (3-k)) (abs).
......@@ -1110,43 +1139,71 @@ let order_record () =
Require Import LibInt.
Lemma rec_partial_half_spec : forall k n,
n = 2 * k ->
n = 2 * k -> k >= 0 ->
app rec_partial_half [n] \[] \[= k].
Proof using.
dup 2.
{ => k. induction_wf IH: (downto 0) k. xcf.
xif.
xrets. xif.
{ xrets. math. }
{ xif.
{ xrets. xif.
{ xfail. math. }
{ xapps (k-1).
{ unfolds. skip.
(* TODO Anomaly: Z.sub is not an evaluable constant.
=> maybe because I made it opaque? *)
}
{ skip. }
{ xrets. skip. } } } }
{ xind_skip as IH. xcf. x.
{ xgo~. }
{ x. { x. math. } { xapps (k-1). skip. x. x. skip. } } }
{ xapps (k-1). math. math. math.
xrets. math. } } }
{ xind_skip as IH. xcf. xrets. xif.
{ xgo~. math. }
{ xrets. xif. math. xapps (k-1). math. math. xrets. math. } }
Qed.
Ltac xuntag_goal_core tt ::=
match goal with
| |- @tag tag_goal _ _ _ _ => unfold tag at 1
| _ => idtac
end.
Lemma rec_mutual_f_and_g_spec :
Ltac xcf_core tt ::=
intros;
xuntag_goal;
match goal with
| |- spec ?f ?n ?P => first [ xcf_core_spec f | xcf_fallback f | fail 2 ]
| |- curried ?n ?f /\ ?P => first [ xcf_core_spec f | xcf_fallback f | fail 2 ]
| |- app ?f ?xs ?H ?Q => first [ xcf_core_app f | xcf_top_value f | xcf_fallback f | fail 2 ]
| |- tag tag_apply (app ?f ?xs) ?H ?Q => first [ xuntag tag_apply; xcf_core_app f | xcf_fallback f | fail 2 ]
| |- ?f = _ => first [ xcf_top_value f | xcf_fallback f | fail 2 ]
| _ => fail 1 "need to call [xcf_show f as H], where [f] is the name of the definition"
end.
(* we can do a simple proof if we are ready to duplicate the verification of [g] *)
Lemma rec_mutual_f_and_g_spec_inlining :
(forall (x:int), x >= 0 -> app rec_mutual_f [x] \[] \[= x])
/\ (forall (x:int), x >= -1 -> app rec_mutual_g [x] \[] \[= x+1]).
Proof using.
intros. cuts G: (forall (m:int),
(forall x, x <= m -> x >= 0 -> app rec_mutual_f [x] \[] \[= x])
/\ (forall x, x+1 <= m -> x >= -1 -> app rec_mutual_g [x] \[] \[= x+1])).
{ split; intros x P; specializes G (x+1); destruct G as [G1 G2]; xapp; try math. }
=> m. induction_wf IH: (downto 0) m. split; intros x Lx Px.
{ xcf. xif. xrets~. xapp (x-1).
unfolds. skip. (* TODO *) skip. skip.
intro_subst. xrets. skip. }
{ xcf. xapp x. unfolds. skip. (* TODO *) skip. skip. }
logic (forall (A B:Prop), A -> (A -> B) -> A /\ B).
{ intros x. induction_wf IH: (downto 0) x. intros Px.
xcf. xif. xrets~. xlet.
xcf. xapp. math. math. xpulls. xrets. math. }
{ intros Sg. introv Px. xcf. xapps. math. }
Qed.
(* the general approach is as follows *)
(* TODO: does not work yet
Lemma rec_mutual_f_and_g_spec :
(forall (x:int), x >= 0 -> app rec_mutual_f [x] \[] \[= x])
/\ (forall (x:int), x >= -1 -> app rec_mutual_g [x] \[] \[= x+1]).
Proof using.
intros. cuts G: (forall (m:int),
(forall x, 0 <= x <= m+1 -> app rec_mutual_f [x] \[] \[= x])
/\ (forall x, -1 <= x <= m-1 -> app rec_mutual_g [x] \[] \[= x+1])).
{ split; intros x P; specializes G (x+4);
destruct G as [G1 G2]; xapp; try math. }
=> m. induction_wf IH: (downto (-2)) m.
specializes IH (m-1). split; intros x (Lx&Px).
{ xcf. xif. xrets~. xapp.
math. split. math. skip. intro_subst. xrets. math. }
{ xcf. xapp. math. math. }
Qed.
*)
(********************************************************************)
......@@ -1161,8 +1218,8 @@ Proof using.
xapp.
xapp.
dup 4.
{ xgc (r3 ~~> 1). skip. }
{ xgc r3. skip. }
{ xgc (_r3 ~~> 1). skip. }
{ xgc _r3. skip. }
{ xgc_but r1. skip. }
{ xlet (fun x => \[x = 2] \* r1 ~~> 1).
{ xapp. xapp. xsimpl~. } (* auto GC on r5 *)
......@@ -1291,7 +1348,7 @@ Qed.
(********************************************************************)
(* ** Arrays *)
Require Import Array_ml Array_proof.
Require Import Array_proof LibListZ.
Section Array.
......@@ -1303,8 +1360,9 @@ Lemma array_ops_spec :
app array_ops [tt] \[] \[= 3].
Proof using.
xcf.
xapp. math. => L EL.
asserts LL: (length L = 3). subst. rewrite length_make; math.
xapp. math. => L EL.
asserts LL: (LibListZ.length L = 3).
{ subst. rewrite LibListZ.length_make; math. }
xapps. { apply index_bounds_impl; math. }
xapp~.
xapps~.
......@@ -1364,10 +1422,10 @@ Proof. reflexivity. Qed.
(* lnot *)
Goal lnot 44 = -45.
Goal Zlnot 44 = -45.
Proof. reflexivity. Qed.
Goal lnot (-44) = 43.
Goal Zlnot (-44) = 43.
Proof. reflexivity. Qed.
(* shiftl *)
......
lib/coq/CFBuiltin.v
View file @ 78e95944
......@@ -24,13 +24,92 @@ Definition array (A:Type) := loc.
(** Values that support polymorphic comparison *)
Axiom is_poly_comparable : forall (A:Type), A -> Prop.
Axiom polymorphic_eq_arg : forall (A:Type), A -> Prop.
Axiom polymorphic_eq_arg_unit : forall (v:unit),
polymorphic_eq_arg v.
Axiom polymorphic_eq_arg_int : forall (n:int),
polymorphic_eq_arg n.
Axiom polymorphic_eq_arg_bool : forall (b:bool),
polymorphic_eq_arg b.
Axiom polymorphic_eq_arg_char : forall (c:char),
polymorphic_eq_arg c.
Axiom polymorphic_eq_arg_string : forall (s:string),
polymorphic_eq_arg s.
Axiom polymorphic_eq_arg_none : forall A,
polymorphic_eq_arg (@None A).
Axiom polymorphic_eq_arg_some : forall A (v:A),
polymorphic_eq_arg v ->
polymorphic_eq_arg (Some v).
Axiom polymorphic_eq_arg_nil : forall A,
polymorphic_eq_arg (@nil A).
Axiom polymorphic_eq_arg_cons : forall A (v:A) (l:list A),
polymorphic_eq_arg v ->
polymorphic_eq_arg l ->
polymorphic_eq_arg (v::l).
Axiom polymorphic_eq_arg_tuple_2 :
forall A1 A2 (v1:A1) (v2:A2),
polymorphic_eq_arg v1 ->
polymorphic_eq_arg v2 ->
polymorphic_eq_arg (v1,v2).
Axiom polymorphic_eq_arg_tuple_3 :
forall A1 A2 A3 (v1:A1) (v2:A2) (v3:A3),
polymorphic_eq_arg v1 ->
polymorphic_eq_arg v2 ->
polymorphic_eq_arg v3 ->
polymorphic_eq_arg (v1,v2,v3).
Axiom polymorphic_eq_arg_tuple_4 :
forall A1 A2 A3 A4 (v1:A1) (v2:A2) (v3:A3) (v4:A4),
polymorphic_eq_arg v1 ->
polymorphic_eq_arg v2 ->
polymorphic_eq_arg v3 ->
polymorphic_eq_arg v4 ->
polymorphic_eq_arg (v1,v2,v3,v4).
Axiom polymorphic_eq_arg_tuple_5 :
forall A1 A2 A3 A4 A5 (v1:A1) (v2:A2) (v3:A3) (v4:A4) (v5:A5),
polymorphic_eq_arg v1 ->
polymorphic_eq_arg v2 ->
polymorphic_eq_arg v3 ->
polymorphic_eq_arg v4 ->
polymorphic_eq_arg v5 ->
polymorphic_eq_arg (v1,v2,v3,v4,v5).
Hint Resolve
polymorphic_eq_arg_unit
polymorphic_eq_arg_int
polymorphic_eq_arg_bool
polymorphic_eq_arg_char
polymorphic_eq_arg_string
polymorphic_eq_arg_none
polymorphic_eq_arg_some
polymorphic_eq_arg_nil
polymorphic_eq_arg_cons
polymorphic_eq_arg_tuple_2
polymorphic_eq_arg_tuple_3
polymorphic_eq_arg_tuple_4
polymorphic_eq_arg_tuple_5
: polymorphic_eq.
(** Tactic [xpolymorphic_eq] attempts to automatically
solves goals of the form [polymorphic_eq_arg v].
Do not use this tactic in the body of a Hint Extern,
because it itself calls [eauto]. *)
Ltac xpolymorphic_eq_core tt :=
eauto with polymorphic_eq.
Tactic Notation "xpolymorphic_eq" :=
xpolymorphic_eq_core tt.
Class PolyComparable (A:Type) (v:A) : Prop :=
{ polyComparable : is_poly_comparable v }.
(********************************************************************)
(* FUTURE USE
Class PolyComparableType (A:Type) : Prop :=
{ polyComparableType : forall (v:A), is_poly_comparable v }.
{ polyComparableType : forall (v:A), polymorphic_eq_arg v }.
Lemma PolyComparableType_eq : forall (A:Type),
PolyComparableType A = (forall (v:A), PolyComparable v).
......@@ -45,128 +124,54 @@ Lemma PolyComparableType_elim : forall `{PolyComparableType A} (v:A),
Proof using. introv. rewrite PolyComparableType_eq. typeclass. Qed.
(* DO NOT add this lemmas as instance, it makes everything slow. *)
Axiom is_poly_comparable_unit : forall (v:unit),
PolyComparable v.
Axiom is_poly_comparable_int : forall (n:int),
PolyComparable n.
Axiom is_poly_comparable_bool : forall (b:bool),
PolyComparable b.
Axiom is_poly_comparable_char : forall (c:char),
PolyComparable c.
Axiom is_poly_comparable_string : forall (s:string),
PolyComparable s.
Existing Instance is_poly_comparable_unit.
Existing Instance is_poly_comparable_int.
Existing Instance is_poly_comparable_bool.
Existing Instance is_poly_comparable_char.
Existing Instance is_poly_comparable_string.
Axiom is_poly_comparable_none : forall A,
PolyComparable (@None A).
Axiom is_poly_comparable_some : forall A (v:A),
PolyComparable v ->
PolyComparable (Some v).
Axiom is_poly_comparable_nil : forall A,
PolyComparable (@nil A).
Axiom is_poly_comparable_cons : forall A (v:A) (l:list A),
PolyComparable v ->
PolyComparable l ->
PolyComparable (v::l).
Existing Instance is_poly_comparable_none.
Existing Instance is_poly_comparable_some.
Existing Instance is_poly_comparable_nil.
Existing Instance is_poly_comparable_cons.
Global Instance is_poly_comparable_type_unit :
Global Instance polymorphic_eq_arg_type_unit :
PolyComparableType unit.
Proof using. rewrite PolyComparableType_eq. typeclass. Qed.
Global Instance is_poly_comparable_type_int :
Global Instance polymorphic_eq_arg_type_int :
PolyComparableType int.
Proof using. rewrite PolyComparableType_eq. typeclass. Qed.
Global Instance is_poly_comparable_type_bool :
Global Instance polymorphic_eq_arg_type_bool :
PolyComparableType bool.
Proof using. rewrite PolyComparableType_eq. typeclass. Qed.
Global Instance is_poly_comparable_type_char :
Global Instance polymorphic_eq_arg_type_char :
PolyComparableType char.
Proof using. rewrite PolyComparableType_eq. typeclass. Qed.
Global Instance is_poly_comparable_type_string :
Global Instance polymorphic_eq_arg_type_string :
PolyComparableType string.
Proof using. rewrite PolyComparableType_eq. typeclass. Qed.
Global Instance is_poly_comparable_type_option : forall `{PolyComparableType A},
Global Instance polymorphic_eq_arg_type_option : forall `{PolyComparableType A},
PolyComparableType (option A).
Proof using.
introv. do 2 rewrite PolyComparableType_eq. intros.
destruct v; typeclass.
Qed.
Global Instance is_poly_comparable_type_list : forall `{PolyComparableType A},
Global Instance polymorphic_eq_arg_type_list : forall `{PolyComparableType A},
PolyComparableType (list A).
Proof using.
introv. do 2 rewrite PolyComparableType_eq. intros H l.
induction l; typeclass.
Qed.
Axiom is_poly_comparable_tuple_2 :
forall A1 A2 (v1:A1) (v2:A2),
PolyComparable v1 ->
PolyComparable v2 ->
PolyComparable (v1,v2).
Axiom is_poly_comparable_tuple_3 :
forall A1 A2 A3 (v1:A1) (v2:A2) (v3:A3),
PolyComparable v1 ->
PolyComparable v2 ->
PolyComparable v3 ->
PolyComparable (v1,v2,v3).
Axiom is_poly_comparable_tuple_4 :
forall A1 A2 A3 A4 (v1:A1) (v2:A2) (v3:A3) (v4:A4),
PolyComparable v1 ->
PolyComparable v2 ->
PolyComparable v3 ->
PolyComparable v4 ->
PolyComparable (v1,v2,v3,v4).
Axiom is_poly_comparable_tuple_5 :
forall A1 A2 A3 A4 A5 (v1:A1) (v2:A2) (v3:A3) (v4:A4) (v5:A5),
PolyComparable v1 ->
PolyComparable v2 ->
PolyComparable v3 ->
PolyComparable v4 ->
PolyComparable v5 ->
PolyComparable (v1,v2,v3,v4,v5).
Existing Instance is_poly_comparable_tuple_2.
Existing Instance is_poly_comparable_tuple_3.
Existing Instance is_poly_comparable_tuple_4.
Existing Instance is_poly_comparable_tuple_5.
(* deprecated
Existing Instance is_poly_comparable_type_option.
Existing Instance is_poly_comparable_type_list.
*)
Global Instance is_poly_comparable_type_tuple_2 :
Global Instance polymorphic_eq_arg_type_tuple_2 :
forall `{PolyComparableType A1} `{PolyComparableType A2},
PolyComparableType (A1 * A2)%type.
Proof using.
intros. rewrite PolyComparableType_eq in *.
intros (v1&v2). typeclass.
Qed.
Global Instance is_poly_comparable_type_tuple_3 :
Global Instance polymorphic_eq_arg_type_tuple_3 :
forall `{PolyComparableType A1} `{PolyComparableType A2} `{PolyComparableType A3},
PolyComparableType (A1 * A2 * A3)%type.
Proof using.
intros. rewrite PolyComparableType_eq in *.
intros [[v1 v2] v3]. typeclass.
Qed.
Global Instance is_poly_comparable_type_tuple_4 :
Global Instance polymorphic_eq_arg_type_tuple_4 :
forall `{PolyComparableType A1} `{PolyComparableType A2} `{PolyComparableType A3}
`{PolyComparableType A4},
PolyComparableType (A1 * A2 * A3 * A4)%type.
......@@ -174,7 +179,7 @@ Proof using.
intros. rewrite PolyComparableType_eq in *.
intros [[[v1 v2] v3] v4]. typeclass.
Qed.
Global Instance is_poly_comparable_type_tuple_5 :
Global Instance polymorphic_eq_arg_type_tuple_5 :
forall `{PolyComparableType A1} `{PolyComparableType A2} `{PolyComparableType A3}
`{PolyComparableType A4} `{PolyComparableType A5},
PolyComparableType (A1 * A2 * A3 * A4 * A5)%type.
......@@ -183,6 +188,7 @@ Proof using.
intros [[[[v1 v2] v3] v4] v5]. typeclass.
Qed.