Commit 66aab3ab authored by charguer's avatar charguer
Browse files

loops improved

parent 0429b12c
......@@ -9,14 +9,10 @@
(While F1 Do F2 Done_) H (# Hexists X, I false X).
-- xfor_inv prefers to use b-1 as upper bound if possible
-- xapp as b'
-- xapp on a leaf does not do xpull
- xfor_inv tag goal
-- case_if checking single goal
-- xmatch_no_intros should do the inversion.
......@@ -54,6 +50,8 @@
- remettre les vrais noms des external
- todo: test xif new variants
- todo: test xand
- xclose with args for the change.
......@@ -72,8 +70,6 @@ Notation "\aset{ x : A | P }" := (@set_st A (fun x => P))
- generate inhab instance for algebraic
- xwhile needs to call tag_pre_post in branches
- hint spec based on type args
......@@ -229,3 +225,8 @@ MAKEFILE BEAUTIFY
omega requires Z.sub to be transparent, but this is an issue for simpl.
##################################################################
# DEPRECATED
......@@ -694,6 +694,13 @@ let while_false () =
(* ** For loops *)
let for_to_incr r =
let n = ref 0 in
for i = 1 to r do
incr n;
done;
!n
let for_to_incr_pred r =
let n = ref 0 in
for i = 0 to pred r do
incr n;
......@@ -873,3 +880,57 @@ end
(********************************************************************)
(* ** TODO: import of auxiliary files, like in examples/DemoMake *)
(********************************************************************)
(********************************************************************)
(********************************************************************)
(* IN PROGRESS *)
(********************************************************************)
(* ** Comparison operators *)
(* TODO
let compare_int () =
(1 <> 0 && 1 <= 2) || (0 = 1 && 1 >= 2 && 1 < 2 && 2 > 1)
let compare_min () =
(min 0 1)
*)
(********************************************************************)
(* ** List operators *)
(* TODO
let list_ops () =
let x = [1] in
List.length (List.rev (List.concat (List.append [x] [x; x])))
*)
(********************************************************************)
(* ** Advanced pattern matching *)
(* TODO
let match_term_when () =
let f x = x + 1 in
match f 3 with
| 0 -> 1
| n when n > 0 -> 2
| _ -> 3
(* captures (Some x, _) or (_, Some x) with x > 0 *)
let match_or_clauses p =
match p with
| (None, None) -> false
| ((Some x, _) | (_, Some x)) when x > 0 -> true
| (Some x, _) | (_, Some x) -> false
*)
\ No newline at end of file
......@@ -2,273 +2,15 @@ Set Implicit Arguments.
Require Import CFLib.
Require Import Demo_ml.
Require Import Stdlib.
Import ZsubNoSimpl.
Open Scope tag_scope.
(*
Notation "P1 '==>' P2" :=
(@pred_le heap P1 P2) (at level 55,
format "'[' '[' P1 ']' '/' '==>' '/' '[' P2 ']' ']'" )
: charac.
Notation "Q1 '===>' Q2" :=
(@rel_le _ heap Q1 Q2) (at level 69,
format "'[' '[' Q1 ']' '/' '===>' '/' '[' Q2 ']' ']'")
: charac.
*)
(********************************************************************)
(********************************************************************)
(*----
DEMO
(* 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.
Ltac auto_star ::= subst; intuition eauto with maths.
Lemma while_decr_spec' :
app while_decr [tt] \[] \[= 3].
Proof using.
xcf.
xapps. xapps.
xwhile_inv_basic (fun b k => \[k >= 0] \* \[b = isTrue (k > 0)]
\* n ~~> k \* c ~~> (3-k)) (downto 0).
xgo*.
intros. xpull. intros. xgo*.
intros. xpull. intros. xgo*.
xgo*.
intros. xpull. intros. xgo*.
Qed.
Proof using.
xgo.
xwhile_inv_basic (fun b k => \[k >= 0] \* \[b = isTrue (k > 0)]
\* n ~~> k \* c ~~> (3-k)) (downto 0).
xgo*.
xgo*.
Qed.
Lemma while_decr_spec :
app while_decr [tt] \[] \[= 3].
Proof using.
xcf.
(* xlet. xapp1. xapp2. apply Spec. simpl. *)
xapp.
xapp.
xseq.
{ xwhile_inv_basic (fun b k => \[k >= 0] \* \[b = isTrue (k > 0)]
\* n ~~> k \* c ~~> (3-k)) (downto 0).
{ xsimpl*. math. }
{ xtag_pre_post. intros b k. xpull ;=> Hk Hb. xapps. xrets. xauto*. math. }
{ xtag_pre_post. intros k. xpull ;=> Hk Hb. xapps. xapps. simpl. xsimpl. math. eauto. math. math. }
}
xpull. => k Hk Hb. fold_bool. xclean. xapp. xsimpl. math.
Abort.
----*)
(********************************************************************)
(********************************************************************)
(*
todo: test xif new variants
todo: test xand
*)
Ltac xuntag_pre_post_core tt ::=
match goal with
| |- @tag tag_goal _ _ _ _ => unfold tag at 1
| _ => idtac
end.
Ltac xcf_core tt ::=
intros;
xuntag_pre_post;
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.
(* todo cleanup*)
Hint Rewrite downto_def nat_upto_wf upto_def : rew_maths.
(* 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.
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, using a measure *)
Lemma rec_mutual_f_and_g_spec_measure :
(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, -1 <= x /\ 2*x <= m -> app rec_mutual_f [x] \[] \[= x])
/\ (forall x, -1 <= x /\ 2*x+3 <= m -> app rec_mutual_g [x] \[] \[= x+1])).
{ split; intros x P; specializes G (2*x+3);
destruct G as [G1 G2]; xapp; try math. }
=> m. induction_wf IH: (downto (-1)) m.
specializes IH (m-1). split; intros x (Lx&Px).
{ xcf. xif. xrets~. xapp. math. math.
intro_subst. xrets. math. }
{ xcf. xapp. math. math. }
Qed.
(* the general approach is as follows, using a lexicographical order
--- LATER
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.
Search lexico2.
set (R := lexico2 (downto (-1)) (downto (-1))).
intros. cuts G: (forall p,
(forall x, -1 <= x /\ R (x,0) p -> app rec_mutual_f [x] \[] \[= x])
/\ (forall x, -1 <= x /\ R (x+1,1) p -> app rec_mutual_g [x] \[] \[= x+1])).
{ split; intros x P.
{ specializes G (x+1,0). destruct G as [G1 G2]. xapp.
unfold R, lexico2. split. math. left. math. }
{ specializes G (x+2,0). destruct G as [G1 G2]. xapp.
unfold R, lexico2. split. math. left. math. } }
=> p. induction_wf IH: R p. split; intros x (Lx&Px).
destruct p as [a b]. unfolds R, @lexico2.
{ xcf. xif. xrets~. xapp (x-1,1).
(* todo: lexico2 is defined in a too strong way... *)
right. math. math.
intro_subst. xrets. math. }
{ xcf. xapp. math. math. }
Qed.
*)
(********************************************************************)
(********************************************************************)
(********************************************************************)
(* TODO
let compare_int () =
(1 <> 0 && 1 <= 2) || (0 = 1 && 1 >= 2 && 1 < 2 && 2 > 1)
let compare_min () =
(min 0 1)
(********************************************************************)
(* ** List operators *)
let list_ops () =
let x = [1] in
List.length (List.rev (List.concat (List.append [x] [x; x])))
*)
(*
let match_term_when () =
let f x = x + 1 in
match f 3 with
| 0 -> 1
| n when n > 0 -> 2
| _ -> 3
(* captures (Some x, _) or (_, Some x) with x > 0 *)
let match_or_clauses p =
match p with
| (None, None) -> false
| ((Some x, _) | (_, Some x)) when x > 0 -> true
| (Some x, _) | (_, Some x) -> false
*)
(********************************************************************)
(********************************************************************)
(********************************************************************)
(********************************************************************)
(* ** Encoding of names *)
......@@ -1122,29 +864,67 @@ Proof using.
Qed.
(********************************************************************)
(* ** While loops *)
(* ** Evaluation order *)
(* TODO: fix hack *)
Lemma order_app_spec :
app order_app [tt] \[] \[= 2].
Proof using.
dup 2.
{
xcf. xapps. xfun. xfun. xfun.
xapps. { xapps. xrets~. } xpulls.
xapps. { xassert. xapps. xrets~. xapps. xrets~. } xpulls.
xapps. { xassert. xapps. xrets~. xfun.
xrets~ (fun f => \[AppCurried f [a b] := (Ret (a + b)%I)] \* r ~~> 2). eauto. }
xpull ;=> Hf.
xapp. xrets~.
(* TODO: can we make xret guess the post?
The idea is to have [(Ret f) H ?Q] where [f:func] and [f] has a spec in hyps
to instantiate Q with [fun f => H \* \[spec of f]].
Then, the proof should just be [xgo~]. *)
}
{ xcf_go*. skip. (* TODO *) }
Qed.
Definition Zsub := Zminus.
Lemma order_constr_spec :
app order_constr [tt] \[] \[= 1::1::nil].
Proof using.
xcf_go*.
Qed.
(* Details:
xcf. xapps. xfun. xfun.
xapps. { xapps. xrets~. } xpulls.
xapps. { xassert. xapps. xrets~. xrets~. } xpulls.
xrets~.
*)
Infix "-" := Zsub : Int_scope.
Open Scope Int_scope.
Lemma order_list_spec :
app order_list [tt] \[] \[= 1::1::nil].
Proof using. xcf_go*. Qed.
Lemma order_tuple_spec :
app order_tuple [tt] \[] \[= (1,1)].
Proof using. xcf_go*. Qed.
Lemma Zsub_eq : Zsub = Zminus.
Proof using. auto. Qed.
(* TODO:
let order_array () =
Opaque Zsub.
let order_record () =
let r = ref 0 in
let g () = incr r; [] in
let f () = assert (!r = 1); 1 in
{ nb = f(); items = g() }
*)
Hint Rewrite Zsub_eq : rew_maths.
(* end hack *)
(* TODO: move *)
Hint Rewrite downto_def nat_upto_wf upto_def : rew_maths.
(********************************************************************)
(* ** While loops *)
Lemma while_decr_spec :
app while_decr [tt] \[] \[= 3].
......@@ -1217,11 +997,96 @@ Qed.
(*---- TODO: sort out
Ltac auto_star ::= subst; intuition eauto with maths.
Lemma while_decr_spec' :
app while_decr [tt] \[] \[= 3].
Proof using.
xcf.
xapps. xapps.
xwhile_inv_basic (fun b k => \[k >= 0] \* \[b = isTrue (k > 0)]
\* n ~~> k \* c ~~> (3-k)) (downto 0).
xgo*.
intros. xpull. intros. xgo*.
intros. xpull. intros. xgo*.
xgo*.
intros. xpull. intros. xgo*.
Qed.
Proof using.
xgo.
xwhile_inv_basic (fun b k => \[k >= 0] \* \[b = isTrue (k > 0)]
\* n ~~> k \* c ~~> (3-k)) (downto 0).
xgo*.
xgo*.
Qed.
Lemma while_decr_spec :
app while_decr [tt] \[] \[= 3].
Proof using.
xcf.
(* xlet. xapp1. xapp2. apply Spec. simpl. *)
xapp.
xapp.
xseq.
{ xwhile_inv_basic (fun b k => \[k >= 0] \* \[b = isTrue (k > 0)]
\* n ~~> k \* c ~~> (3-k)) (downto 0).
{ xsimpl*. math. }
{ xtag_pre_post. intros b k. xpull ;=> Hk Hb. xapps. xrets. xauto*. math. }
{ xtag_pre_post. intros k. xpull ;=> Hk Hb. xapps. xapps. simpl. xsimpl. math. eauto. math. math. }
}
xpull. => k Hk Hb. fold_bool. xclean. xapp. xsimpl. math.
Abort.
----*)
(********************************************************************)
(* ** For loops *)
Lemma for_to_incr_spec : forall (r:int), r >= 0 ->
Lemma for_to_incr_spec : forall (r:int), r >= 1 ->
app for_to_incr [r] \[] \[= r].
Proof using.
xcf. xapps. dup 7.
{ xfor. intros S LS HS.
cuts PS: (forall i, (i <= r+1) -> S i (n ~~> (i-1)) (# n ~~> r)).
{ applys PS. math. }
{ intros i. induction_wf IH: (upto (r+1)) i. intros Li.
applys (rm HS). xif.
{ xapps. applys_eq IH 2. hnf. math. math. fequals_rec. math. }
{ xrets. math. } }
xapps. xsimpl~. }
{ xfor as S. skip. skip. }
{ xfor_inv (fun (i:int) => n ~~> (i-1)).
{ math. }
{ xsimpl. }
{ introv L. simpl. xapps. xsimpl. math. }
xapps. xsimpl. math. }
{ xseq (# n ~~> r). xfor_inv (fun (i:int) => n ~~> (i-1)).
skip. skip. skip. skip. skip. }
{ xseq (# n ~~> r). xfor_inv_void. skip. skip. skip. }
{ xfor_inv_void. skip. skip. }
{ try xfor_inv_case (fun (i:int) => n ~~> (i-1)).
(* fails because no post condition *)
xseq (# n ~~> r).
{ xfor_inv_case (fun (i:int) => n ~~> (i-1)).
{ xsimpl. }
{ introv L. xapps. xsimpl. math. }
{ xsimpl. math. }
{ math_rewrite (r = 0). xsimpl. } }
{ xapps. xsimpl~. } }
Abort.
Lemma for_to_incr_pred_spec : forall (r:int), r >= 1 ->
app for_to_incr_pred [r] \[] \[= r].
Proof using.
xcf. xapps. dup 7.
{ xfor. intros S LS HS.
......@@ -1229,14 +1094,14 @@ Proof using.
{ applys PS. math. }
{ intros i. induction_wf IH: (upto r) i. intros Li.
applys (rm HS). xif.
{ xapps. applys IH. hnf. math. math. }
{ xapps. applys_eq IH 2. hnf. math. math. auto. }
{ xrets. math. } }
xapps. xsimpl~. }
{ xfor as S. skip. skip. }
{ xfor_inv (fun (i:int) => n ~~> i).
{ math. }
{ xsimpl. }
{ introv L. xapps. }
{ introv L. simpl. xapps. }
xapps. xsimpl. math. }
{ xseq (# n ~~> r). xfor_inv (fun (i:int) => n ~~> i).
skip. skip. skip. skip. skip. }
......@@ -1248,7 +1113,7 @@ Proof using.
{ xfor_inv_case (fun (i:int) => n ~~> i).
{ xsimpl. }
{ introv L. xapps. }
{ xsimpl. math. }
{ xsimpl. }
{ math_rewrite (r = 0). xsimpl. } }
{ xapps. xsimpl~. } }
Abort.
......@@ -1288,62 +1153,6 @@ Abort.
(********************************************************************)
(* ** Evaluation order *)
Lemma order_app_spec :
app order_app [tt] \[] \[= 2].
Proof using.
dup 2.
{
xcf. xapps. xfun. xfun. xfun.
xapps. { xapps. xrets~. } xpulls.