Commit b6882e9e authored by Benoit Viguier's avatar Benoit Viguier
Browse files

update

parent 53da05db
Set Warnings "-notation-overridden".
Require Import Coq.ZArith.ZArith.
Require Import Coq.FSets.FMaps.
Require Import Coq.Lists.List.
Require Import Coq.Program.Program.
Open Scope Z_scope.
......@@ -136,10 +136,43 @@ Fixpoint expr_denote env (m : expr) : Z :=
| Add x y => (expr_denote env x + expr_denote env y)%Z
end.
Fixpoint list_subst_expr (l : list expr) (v v' : term) : list expr :=
match l with
| nil => nil
| h :: q => subst_expr h v v' :: list_subst_expr q v v'
end.
Fixpoint subst_all_list_expr (x : list expr) (xs : list (term * term)) : list expr :=
match xs with
| nil => x
| cons (v, v') xs =>
subst_all_list_expr (list_subst_expr x v v') xs
end.
Lemma subst_all_list_expr_nil defs :
subst_all_list_expr nil defs = nil.
Proof.
induction defs; simpl; intros; auto.
destruct a.
rewrite IHdefs; reflexivity.
Qed.
Lemma subst_all_list_expr_cons defs : forall x y,
subst_all_list_expr (x :: y) defs =
(subst_all_expr x defs) :: (subst_all_list_expr y defs).
Proof.
induction defs; simpl; intros; auto.
destruct a.
rewrite IHdefs; reflexivity.
Qed.
Definition list_expr_denote env (l :list expr) : list Z := map (expr_denote env) l.
Inductive formula :=
| Top : formula
| Bottom : formula
| Equal : expr -> expr -> formula
| Equal_L : list expr -> list expr -> formula
| Impl : formula -> formula -> formula.
Fixpoint subst_formula (t : formula) (v v' : term) : formula :=
......@@ -147,6 +180,7 @@ Fixpoint subst_formula (t : formula) (v v' : term) : formula :=
| Top => Top
| Bottom => Bottom
| Equal x y => Equal (subst_expr x v v') (subst_expr y v v')
| Equal_L x y => Equal_L (list_subst_expr x v v') (list_subst_expr y v v')
| Impl p q => Impl (subst_formula p v v') (subst_formula q v v')
end.
......@@ -173,6 +207,15 @@ Proof.
rewrite IHdefs; reflexivity.
Qed.
Lemma subst_all_formula_Equal_L defs : forall x y,
subst_all_formula (Equal_L x y) defs =
Equal_L (subst_all_list_expr x defs) (subst_all_list_expr y defs).
Proof.
induction defs; simpl; intros; auto.
destruct a.
rewrite IHdefs; reflexivity.
Qed.
Lemma subst_all_formula_Equal defs : forall x y,
subst_all_formula (Equal x y) defs =
Equal (subst_all_expr x defs) (subst_all_expr y defs).
......@@ -196,6 +239,7 @@ Fixpoint formula_denote env (t : formula) : Prop :=
| Top => True
| Bottom => False
| Equal x y => expr_denote env x = expr_denote env y
| Equal_L x y => list_expr_denote env x = list_expr_denote env y
| Impl p q => formula_denote env p -> formula_denote env q
end.
......@@ -210,11 +254,18 @@ Fixpoint expr_size (t : expr) : nat :=
| Add x y => 1%nat + expr_size x + expr_size y
end.
Fixpoint list_expr_size (l: list expr) : nat :=
match l with
|nil => 1%nat
| h :: q => 1%nat + expr_size h + list_expr_size q
end.
Fixpoint formula_size (t : formula) : nat :=
match t with
| Top => 1%nat
| Bottom => 1%nat
| Equal x y => 1%nat + expr_size x + expr_size y
| Equal_L x y => 1%nat + list_expr_size x + list_expr_size y
| Impl p q => formula_size p + formula_size q
end.
......@@ -230,6 +281,15 @@ Proof.
- rewrite subst_all_expr_Add; simpl; auto.
Qed.
Lemma expr_size_subst_all_list_expr defs m :
list_expr_size (subst_all_list_expr m defs) = list_expr_size m.
Proof.
induction m; simpl.
- rewrite subst_all_list_expr_nil; simpl; auto.
- rewrite subst_all_list_expr_cons; simpl;
rewrite expr_size_subst_all_expr; auto.
Qed.
Lemma formula_size_subst_all_formula defs q :
formula_size (subst_all_formula q defs) = formula_size q.
Proof.
......@@ -238,6 +298,8 @@ Proof.
- rewrite subst_all_formula_Bottom; simpl; auto.
- rewrite subst_all_formula_Equal; simpl; auto.
rewrite !expr_size_subst_all_expr; auto.
- rewrite subst_all_formula_Equal_L; simpl; auto.
repeat rewrite expr_size_subst_all_list_expr; auto.
- rewrite subst_all_formula_Impl; simpl; auto.
Qed.
......@@ -313,6 +375,17 @@ Proof.
rewrite IHt1, IHt2; auto.
Qed.
Lemma list_expr_substitution_eq env t xs :
Forall (fun p => term_denote env (fst p) = term_denote env (snd p)) xs
-> list_expr_denote env (subst_all_list_expr t (substitutions xs)) =
list_expr_denote env t.
Proof.
induction t; simpl; intros.
- rewrite subst_all_list_expr_nil ; simpl ; auto.
- rewrite subst_all_list_expr_cons ; simpl.
rewrite expr_substitution_eq, IHt; auto.
Qed.
Lemma formula_substitution_eq env t xs :
Forall (fun p => term_denote env (fst p) = term_denote env (snd p)) xs
-> formula_denote env (subst_all_formula t (substitutions xs)) =
......@@ -323,6 +396,8 @@ Proof.
- rewrite subst_all_formula_Bottom; simpl; auto.
- rewrite subst_all_formula_Equal; simpl; intros.
rewrite !expr_substitution_eq; auto.
- rewrite subst_all_formula_Equal_L; simpl; intros.
rewrite !list_expr_substitution_eq; auto.
- rewrite subst_all_formula_Impl; simpl; intros.
intuition.
rewrite H0, H1; auto.
......@@ -332,23 +407,48 @@ Qed.
* Computational decision procedure for map membership
*)
Definition decision (env : environment) (m n : expr) : bool :=
Z.eqb (expr_denote env m) (expr_denote env n).
Lemma decision_eq : forall env x y, decision env x y = true -> expr_denote env x = expr_denote env y.
Proof. intros ; unfold decision in H ; apply Z.eqb_eq in H ; auto. Qed.
Fixpoint list_decision (env : environment) (m n : list expr) : bool :=
match m,n with
| nil,nil => true
| h1::q1, h2::q2 => decision env h1 h2 && list_decision env q1 q2
| _ , _ => false
end.
Lemma list_decision_eq : forall env n m, list_decision env m n = true ->
list_expr_denote env m = list_expr_denote env n.
Proof.
induction n ; intros [] Heq ; simpl in * ; try congruence.
apply Bool.andb_true_iff in Heq ; destruct Heq as [Hdec Hlistdec].
f_equal.
apply decision_eq ; assumption.
auto.
Qed.
Program Definition formula_forward (t : formula) env (hyp : formula)
(cont : forall env' defs, [formula_denote env' (subst_all_formula t defs)]) :
[formula_denote env hyp -> formula_denote env t] :=
match hyp with
| Top => Reduce (cont env nil)
| Bottom => Yes
| Equal x y => No (* Benoit: TODO *)
(* | Equal x y => match x,y with
| Ref a,Ref b => Reduce (cont env [(a,b)])
| _, _ => Reduce (cont env nil)
*)
| Equal x y => No (* TODO *)
| Equal_L x y => No (* TODO *)
| Impl _ _ => Reduce (cont env nil)
end.
Next Obligation.
contradiction.
Defined.
(* Benoit: TODO: This should be changed to fit your problem. *)
Definition decision (env : environment) (m n : expr) : bool :=
Z.eqb (expr_denote env m) (expr_denote env n).
Program Fixpoint formula_backward (t : formula) env {measure (formula_size t)} :
[formula_denote env t] :=
match t with
......@@ -358,15 +458,19 @@ Program Fixpoint formula_backward (t : formula) env {measure (formula_size t)} :
| true => Yes
| false => No
end
| Equal_L x y => match list_decision env x y with
| true => Yes
| false => No
end
| Impl p q =>
formula_forward q env p
(fun env' defs' => formula_backward (subst_all_formula q defs') env')
end.
Next Obligation.
unfold decision in Heq_anonymous.
symmetry in Heq_anonymous.
apply Z.eqb_eq in Heq_anonymous.
assumption.
apply decision_eq ; auto.
Defined.
Next Obligation.
apply list_decision_eq ; auto.
Defined.
Next Obligation.
rewrite formula_size_subst_all_formula; simpl.
......@@ -437,13 +541,19 @@ Ltac allVars xs e :=
| ?X + ?Y =>
let xs := allVar xs X in
allVar xs Y
| nil = nil => xs
| ?hp :: ?qp = ?hq :: ?qq =>
let xs1 := allVars xs hp in
let xs2 := allVars xs1 qp in
let xs3 := allVars xs2 hq in
allVars xs3 qq
| ?P = ?Q =>
let xs := allVars xs P in
allVars xs Q
| ?P -> ?Q =>
let xs := allVars xs P in
allVars xs Q
| ?X => allVar xs X (* Benoit: TODO: This may be too open *)
(* | ?X => allVar xs X (* Benoit: TODO: This may be too open *)*)
| _ => xs
end.
......@@ -473,6 +583,11 @@ Ltac reifyExpr env t :=
let x := reifyExpr env X in
let y := reifyExpr env Y in
constr:(Add x y)
| nil => constr:(nil)
| ?X :: ?Y =>
let x := reifyExpr env X in
let y := reifyExpr env Y in
constr:(cons x y)
| ?X =>
let x := reifyValue env X in
constr:(Ref x)
......@@ -524,7 +639,11 @@ Ltac reify :=
*)
Ltac maths := reify; apply formula_sound; vm_compute; auto.
Goal 2 * 3 = 3 * 2.
maths.
Qed.
(*
Goal forall x, (2*3*4*x = 3*4*2*x)%Z.
intros.
reify.
apply formula_sound.
vm_compute.
Qed.*)
\ No newline at end of file
......@@ -53,7 +53,7 @@ COQTOP=$(COQBIN)coqtop
COQDEP=$(COQBIN)coqdep $(DEPFLAGS)
COQDOC=$(COQBIN)coqdoc -d doc -g -utf8 $(DEPFLAGS)
COQVERSION= 8.6
COQVERSION= 8.6.1
COQV=$(shell $(COQC) -v)
ifeq ("$(filter $(COQVERSION),$(COQV))","")
$(error FAILURE: You need Coq $(COQVERSION) but you have this version: $(COQV))
......
......@@ -10,7 +10,7 @@ Definition update_M_i_j' (i j:nat) (a:Z) b o := list_alter (local_update_M j a b
Function inner_M_fix (i j a:Z) (b o : list Z) {measure Z.to_nat j} : list Z :=
if (j <=? 0) then o else inner_M_fix i (j - 1) a b (update_M_i_j i (j - 1) a b o).
Proof. intros. apply Z2Nat.inj_lt ; rewrite Z.leb_gt in teq; omega. Qed.
Proof. intros. apply Z2Nat.inj_lt ; rewrite Z.leb_gt in teq; omega. Defined.
Fixpoint inner_M_fix' (i j : nat) (a:Z) (b o : list Z) := match j with
| 0%nat => o
......
......@@ -7,18 +7,6 @@ Require Import stdpp.prelude.
Local Open Scope Z.
Lemma ZscalarMult_bound_const: forall (m2 n2 o p a: Z) (b: list Z),
0 <= a ->
Forall (fun x => m2 <= x <= n2) b ->
o = a * m2 ->
p = a * n2 ->
Forall (fun x => o <= x <= p) (a ∘∘ b).
Proof.
introv Ha Hb Ho Hp.
rewrite ZscalarMult_eq_ZunopList.
eapply (Forall_ZunopList _ (fun x : => a = x) (fun x : => m2 <= x <= n2)) ; go.
Qed.
Lemma ZscalarMult_bound_inter: forall (m1 n1 m2 n2 o p a: Z) (b: list Z),
(fun x => m1 <= x <= n1) a ->
Forall (fun x => m2 <= x <= n2) b ->
......
......@@ -9,7 +9,7 @@ Function outer_M_fix (i j : Z) (a b o : list Z) {measure Z.to_nat i} : list Z :
if (i <=? 0)
then (inner_M_fix 0 j (from_option id 0 (a !! (Z.to_nat 0))) b o)
else outer_M_fix (i - 1) 16 a b (inner_M_fix i j (from_option id 0 (a !! (Z.to_nat i))) b o).
Proof. intros. apply Z2Nat.inj_lt ; rewrite Z.leb_gt in teq; omega. Qed.
Proof. intros. apply Z2Nat.inj_lt ; rewrite Z.leb_gt in teq; omega. Defined.
Fixpoint outer_M_fix' (i j : nat) (a b o : list Z) := match i with
| 0%nat => (inner_M_fix' 0%nat j (from_option id 0 (a !! 0%nat)) b o)
......
......@@ -53,4 +53,17 @@ Qed.
End Integer.
Lemma ZscalarMult_bound_const: forall (m2 n2 o p a: Z) (b: list Z),
0 <= a ->
Forall (fun x => m2 <= x <= n2) b ->
o = a * m2 ->
p = a * n2 ->
Forall (fun x => o <= x <= p) (a ∘∘ b).
Proof.
introv Ha Hb Ho Hp.
rewrite ZscalarMult_eq_ZunopList.
eapply (Forall_ZunopList _ (fun x : => a = x) (fun x : => m2 <= x <= n2)) ; go.
Qed.
Close Scope Z.
......@@ -9,14 +9,14 @@
sudo apt-get install gcc
sudo apt-get install opam
opam init
opam switch 4.04.1
opam switch 4.05.0
````
##### 2. install coq 8.6 + coqide + ssreflect
````bash
opam install coq.8.6
opam install coqide.8.6
opam install coq
opam install coqide
opam repo add coq-released https://coq.inria.fr/opam/released
opam repo add coq-extra-dev https://coq.inria.fr/opam/extra-dev
# opam install coq-mathcomp-ssreflect.1.6.1
......
......@@ -80,10 +80,10 @@ Qed.
Close Scope Z.
Corollary Unpack25519_length_16_32 : forall l, length l = 32 -> length (unpack_for 16 l) = 16.
Corollary Unpack25519_length_16_32 : forall l, length l = 32 -> length (unpack_for 8 l) = 16.
Proof.
intros.
rewrite (Unpack25519_length 16) with (m:=32).
rewrite (Unpack25519_length 8) with (m:=32).
reflexivity.
omega.
assumption.
......
Supports Markdown
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