Commit 47c00276 authored by charguer's avatar charguer

definitions for cf_for, cf_for_down, and cf_while

parent fb80be3c
.PHONY: all coqlib generator examples doc clean install uninstall reinstall
CFML := $(shell pwd)
CFML := $(shell pwd)
##############################################################################
# Installation destinations.
......
......@@ -9,6 +9,7 @@
-include $(CFML)/settings.sh
############################################################################
# We assume that TLC has been installed.
# (Note: this definition can be overriden from outside.)
......
opam switch 4.03.0
eval `opam config env`
(* TODO: why jauto does clearbody? *)
......
......@@ -205,6 +205,17 @@ let rec coqtops_of_imp_cf cf =
(* (!S: fun H Q => exists Q', F1 H Q /\ F2 (Q' tt) Q *)
| Cf_for (dir,i_name,v1,v2,cf) ->
let c = Coq_fun ((i_name, coq_int), coq_of_cf cf) in
let tag, cf_for =
match dir with
| For_loop_up -> "tag_for", "CFML.CFPrint.cf_for"
| For_loop_down -> "tag_for_down", "CFML.CFPrint.cf_for_down"
in
let f_core = coq_apps (coq_var cf_for) [v1;v2;c] in
let f = Coq_app (Coq_var "CFML.CFHeaps.local", f_core) in
coq_tag tag f
(* DEPRECATED
let s = Coq_var "S" in
let i = Coq_var i_name in
let tag, cond_test, istep =
......@@ -222,7 +233,7 @@ let rec coqtops_of_imp_cf cf =
let bodys = coq_of_cf cf_if in
let hypr = coq_foralls [(i_name, coq_int); ("H", hprop); ("Q", Coq_impl (coq_unit, hprop))] (Coq_impl (coq_apps bodys [h;q], (coq_apps s [i;h;q]))) in
funhq tag (Coq_forall (("S",typs), coq_impls [locals; hypr] (coq_apps s [v1;h;q])))
*)
(* UP:
(!For (fun H Q => forall S:int->~~unit, is_local_pred S ->
(forall i H Q,
......@@ -233,7 +244,7 @@ let rec coqtops_of_imp_cf cf =
-> S v1 H Q)
DOWN:
(!For (fun H Q => forall S:int->~~unit, is_local_pred S ->
(!For (fun H Q => forall S:int->~~unit, is_local_pred S ->
(forall i H Q,
(If_ i >= v2
Then Seq (F1 ;; S (i-1)) H Q))
......@@ -261,6 +272,13 @@ let rec coqtops_of_imp_cf cf =
*)
| Cf_while (cf1,cf2) ->
let c1 = coq_of_cf cf1 in
let c2 = coq_of_cf cf2 in
let f_core = coq_apps (coq_var "CFML.CFPrint.while") [c1;c2] in
let f = Coq_app (Coq_var "CFML.CFHeaps.local", f_core) in
coq_tag "tag_while" f
(*DEPRECATED
let r = Coq_var "R" in
let typr = formula_type in
let cf_step = Cf_seq (cf2, Cf_manual r) in
......@@ -270,6 +288,7 @@ let rec coqtops_of_imp_cf cf =
let hypr = coq_foralls [("H", hprop); ("Q", Coq_impl (coq_unit, hprop))] (Coq_impl (coq_apps bodyr [h;q],(coq_apps r [h;q]))) in
let localr = Coq_app (Coq_var "CFML.CFHeaps.is_local", r) in
funhq "tag_while" (Coq_forall (("R",typr), coq_impls [localr; hypr] (coq_apps r [h;q])))
*)
(* (!While: (fun H Q => forall R:~~unit, is_local R ->
(forall H Q,
(Let _c = F1 in If _c Then (F2 ; R) Ret tt) H Q
......
......@@ -937,6 +937,19 @@ Notation "'Done'" :=
(********************************************************************)
(** While *)
Definition cf_while (F1:~~bool) (F2:~~unit) : ~~unit :=
(fun H Q =>
forall (R:~~unit), is_local R ->
(forall H Q, (LetIf F1 Then (F2 ;; R) Else (Ret tt)) H Q -> R H Q)
-> R H Q).
Notation "'While' F1 'Do' F2 'Done_'" :=
(!While (cf_while F1 F2))
(at level 69, F2 at level 68,
format "'[v' 'While' F1 'Do' '/' '[' F2 ']' '/' 'Done_' ']'")
: charac.
(* DEPRECATED
Notation "'While' F1 'Do' F2 'Done_'" :=
(!While (fun H Q => forall R:~~unit, is_local R ->
(forall H Q, (LetIf F1 Then (F2 ;; R) Else (Ret tt)) H Q -> R H Q)
......@@ -944,11 +957,41 @@ Notation "'While' F1 'Do' F2 'Done_'" :=
(at level 69, F2 at level 68,
format "'[v' 'While' F1 'Do' '/' '[' F2 ']' '/' 'Done_' ']'")
: charac.
*)
(********************************************************************)
(** For *)
Definition cf_for (a:int) (b:int) (F1:int->~~unit) : ~~unit :=
(fun H Q =>
forall (S:int->~~unit), CFHeaps.is_local_pred S ->
(forall i H Q,
(If_ isTrue (i <= (b)%Z) Then (F1 i ;; S (i+1)) Else (Ret tt)) H Q
-> S i H Q)
-> S a H Q).
Notation "'For' i '=' a 'To' b 'Do' F1 'Done_'" :=
(!For (cf_for a b (fun i => F1)))
(at level 69, i ident, a at level 0, b at level 0,
format "'[v' 'For' i '=' a 'To' b 'Do' '/' '[' F1 ']' '/' 'Done_' ']'")
: charac.
Definition cf_for_down (a:int) (b:int) (F1:int->~~unit) : ~~unit :=
(fun H Q =>
forall (S:int->~~unit), CFHeaps.is_local_pred S ->
(forall i H Q,
(If_ isTrue (i >= (b)%Z) Then (F1 i ;; S (i-1)) Else (Ret tt)) H Q
-> S i H Q)
-> S a H Q).
Notation "'For' i '=' a 'DownTo' b 'Do' F1 'Done_'" :=
(!For (cf_for_down a b (fun i => F1)))
(at level 69, i ident, a at level 0, b at level 0,
format "'[v' 'For' i '=' a 'DownTo' b 'Do' '/' '[' F1 ']' '/' 'Done_' ']'")
: charac.
(* DEPRECATED
Notation "'For' i '=' a 'To' b 'Do' F1 'Done_'" :=
(!For (fun H Q => forall S:int->~~unit, CFHeaps.is_local_pred S ->
(forall i H Q,
......@@ -956,7 +999,7 @@ Notation "'For' i '=' a 'To' b 'Do' F1 'Done_'" :=
-> S i H Q)
-> S a H Q))
(at level 69, i ident, a at level 0, b at level 0,
format "'[v' 'For' i '=' a 'To' b 'Do' '/' '[' F1 ']' '/' 'Done_' ']'")
format "'[v' 'For' i '=' a 'Tom' b 'Do' '/' '[' F1 ']' '/' 'Done_' ']'")
: charac.
Notation "'For' i '=' a 'DownTo' b 'Do' F1 'Done_'" :=
......@@ -968,6 +1011,8 @@ Notation "'For' i '=' a 'DownTo' b 'Do' F1 'Done_'" :=
(at level 69, i ident, a at level 0, b at level 0,
format "'[v' 'For' i '=' a 'DownTo' b 'Do' '/' '[' F1 ']' '/' 'Done_' ']'")
: charac.
*)
(********************************************************************)
......
Set Implicit Arguments
Require Import LibNat.
Section NatSimpl.
Open Scope nat_scope.
Implicit Types n : nat.
Lemma nat_zero_plus : forall n,
0 + n = n.
Proof using. intros. math. Qed.
Lemma nat_plus_zero : forall n,
n + 0 = n.
Proof using. intros. math. Qed.
Lemma nat_plus_succ : forall n1 n2,
n1 + S n2 = S (n1 + n2).
Proof using. intros. math. Qed.
Lemma nat_minus_zero : forall n,
n - 0 = n.
Proof using. intros. math. Qed.
Lemma nat_succ_minus_succ : forall n1 n2,
S n1 - S n2 = n1 - n2.
Proof using. intros. math. Qed.
Lemma nat_minus_same : forall n,
n - n = 0.
Proof using. intros. math. Qed.
Lemma nat_plus_minus_same : forall n1 n2,
n1 + n2 - n1 = n2.
Proof using. intros. math. Qed.
End NatSimpl.
Hint Rewrite nat_zero_plus nat_plus_zero nat_plus_succ
nat_minus_zero nat_succ_minus_succ
nat_minus_same nat_plus_minus_same : rew_nat.
Tactic Notation "rew_nat" :=
autorewrite with rew_nat.
Tactic Notation "rew_nat" "in" "*" :=
autorewrite with rew_nat in *.
Tactic Notation "rew_nat" "in" hyp(H) :=
autorewrite with rew_nat in H.
Lemma int_nat_plus : forall (x y:nat),
my_Z_of_nat (x + y)%nat = (my_Z_of_nat x + my_Z_of_nat y).
Proof using. math. Qed.
Lemma int_nat_plus_abs : forall k n,
n >= 0 ->
(k + abs n)%nat = abs (k + n)%Z.
Proof using.
introv N. applys eq_int_nat.
rewrite int_nat_plus.
do 2 (rewrite abs_pos; [|math]).
auto.
Qed.
Lemma nat_int_eq : forall (x y:nat),
(x = y :> nat) -> (x = y :> int).
Proof using. math. Qed.
Require LibListZ.
Module ReadProperties.
Import LibListZ.
Transparent index_inst read_inst.
Lemma read_middle : forall A `{IA:Inhab A} i (L1 L2 : list A) x,
i = length L1 ->
(L1 ++ x :: L2)[i] = x.
Proof.
intros.
unfold LibBag.read, read_inst, read_impl.
unfold nth. case_if. { false; math. }
(* TODO: use new TLC lemmas about nth *)
applys LibList.Nth_to_nth. applys Nth_app_r 0%nat.
constructors. applys eq_int_nat. rewrite abs_pos; math.
Qed.
End ReadProperties.
Import ReadProperties.
\ No newline at end of file
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