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

Add Forall proofs

parent bdbb863f
......@@ -38,7 +38,7 @@ Proof.
Qed.
Lemma Carry_n_step_0 : forall h q a, Carrying_n 0 a (h :: q) = (a + h) :: q.
Proof. intros ; simpl ; flatten ; reflexivity. Qed.
Proof. intros ; simpl; flatten. Qed.
Lemma Carrying_n_length: forall l (m:nat) a, (m < length l)%nat -> length (Carrying_n m a l) = length l.
Proof. induction l as [|h q IHl]; intros [] a Hm; simpl ; flatten ; go. Qed.
......@@ -275,7 +275,7 @@ thus we split it.
Fact factors_256: (2 ^ 256) = (2 ^ 16 * (2 ^ 16 * (2 ^ 16 * (2 ^ 16 * (2 ^ 16 * (2 ^ 16 * (2 ^ 16 * (2 ^ 16 * (2 ^ 16 * (2 ^ 16 * (2 ^ 16 *
(2 ^ 16 * (2 ^ 16 * (2 ^ 16 * (2 ^ 16 * (2 ^ 16)))))))))))))))).
Proof. compute ; reflexivity. Qed.
Fact pre_compute_equality_factor: forall (z z0 z1 z2 z3 z4 z5 z6 z7 z8 z9 z10 z11 z12 z13 z14:Z),
(((((((((((((((z / 2 ^ 16 + z0) / 2 ^ 16 + z1) / 2 ^ 16 + z2) / 2 ^ 16 + z3) / 2 ^ 16 + z4) / 2 ^ 16 + z5) / 2 ^ 16 + z6) / 2 ^ 16 + z7) / 2 ^ 16 + z8) / 2 ^ 16 + z9) / 2 ^ 16 + z10) / 2 ^ 16 + z11) / 2 ^ 16 + z12) / 2 ^ 16 + z13) / 2 ^ 16 + z14) / 2 ^ 16 =
(z + 2 ^ 16 * (z0 + 2 ^ 16 * (z1 + 2 ^ 16 * (z2 + 2 ^ 16 * (z3 + 2 ^ 16 * (z4 + 2 ^ 16 * (z5 + 2 ^ 16 * (z6 + 2 ^ 16 * (z7 + 2 ^ 16 * (z8 + 2 ^ 16 * (z9 + 2 ^ 16 * (z10 + 2 ^ 16 * (z11 + 2 ^ 16 * (z12 + 2 ^ 16 * (z13 + 2 ^ 16 * z14)))))))))))))))
......@@ -406,3 +406,39 @@ Proof.
symmetry.
reflexivity.
Qed.
Lemma BackCarry_fix: forall l, (length l = 16)%nat -> 16.lst l < 2^256 -> car25519 l = Carrying_n 16 15 0 l.
Proof.
intros l H Hl.
unfold car25519.
unfold backCarry.
flatten.
repeat (destruct l ; tryfalse).
repeat rewrite Carry_n_step in Eq.
rewrite Carry_n_step_0 in Eq.
change (0 + z0) with z0.
repeat (destruct l0; tryfalse).
repeat rewrite ListSame in Eq ; jauto_set.
unfold nth.
unfold slice.
f_equal.
admit.
change ([z16; z17; z18; z19; z20; z21; z22; z23; z24; z25; z26; z27; z28; z29; z30]) with
([z16; z17; z18; z19; z20; z21; z22; z23; z24; z25; z26; z27; z28; z29] ++ [z30]).
f_equal.
clear H H0 H1 H2 H3 H4 H5 H6 H7 H8 H9 H10 H11 H12 H13 H14 H16.
unfold getResidute.
Lemma car25519_bound_0 : forall l, (length l = 16)%nat -> nth 0 (car25519 l) 0 < 2 ^ 16.
Lemma car25519_bound_0 : forall l, (length l = 16)%nat -> nth 0 (car25519 l) 0 < 2 ^ 16.
Proof.
destruct i ; intros l H Hi ; [false|].
repeat (destruct l ; tryfalse).
unfold car25519.
unfold backCarry.
Require Import Coq.ZArith.ZArith.
Require Import Coq.ZArith.Znumtheory.
Require Import Coq.Lists.List.
Require Import Coq.Bool.Bool.
Definition in_eq: forall {A: Type} (a:A) l, In a (a::l) :=
fun A a l => or_introl eq_refl.
Definition Forall_forall: forall {A : Type} (P : A -> Prop) (l : list A),
Forall P l <-> (forall x : A, In x l -> P x) :=
fun (A : Type) (P : A -> Prop) (l : list A) =>
conj
(fun H : Forall P l =>
Forall_ind (fun l0 : list A => forall x : A, In x l0 -> P x)
(fun (x : A) (H0 : In x nil) => False_ind (P x) H0)
(fun (x : A) (l0 : list A) (H0 : P x) (_ : Forall P l0)
(IHForall : forall x0 : A, In x0 l0 -> P x0) (x0 : A)
(H2 : In x0 (x :: l0)) =>
or_ind
(fun H3 : x = x0 =>
eq_ind_r (fun x1 : A => P x1 -> P x0) (fun H4 : P x0 => H4) H3 H0)
(fun H3 : In x0 l0 =>
(fun H4 : In x0 l0 -> P x0 => (fun H5 : P x0 => H5) (H4 H3))
(IHForall x0)) H2) H)
(list_ind
(fun l0 : list A => (forall x : A, In x l0 -> P x) -> Forall P l0)
(fun _ : forall x : A, In x nil -> P x => Forall_nil P)
(fun (a : A) (l0 : list A)
(IHl : (forall x : A, In x l0 -> P x) -> Forall P l0)
(H : forall x : A, In x (a :: l0) -> P x) =>
(fun H0 : forall x : A, In x l0 -> P x =>
(fun H1 : forall x : A, In x l0 -> P x =>
(fun H2 : Forall P l0 =>
(fun H3 : A =>
(fun X : A =>
(fun H4 : In X (a :: l0) -> P X =>
(fun (_ : a = X -> P X)
(_ : (fix In (a0 : A) (l1 : list A) {struct l1} : Prop :=
match l1 with
| nil => False
| b :: m => b = a0 \/ In a0 m
end) X l0 -> P X) =>
Forall_cons a (H a (in_eq a l0)) H2)
(fun H5 : a = X => H4 (or_introl H5))
(fun
H5 : (fix In (a0 : A) (l1 : list A) {struct l1} : Prop :=
match l1 with
| nil => False
| b :: m => b = a0 \/ In a0 m
end) X l0 => H4 (or_intror H5))) (H X)) H3) a)
(IHl H1)) H0)
(fun (x : A) (H0 : In x l0) =>
(fun H1 : In x (a :: l0) -> P x =>
(fun (_ : a = x -> P x)
(H3 : (fix In (a0 : A) (l1 : list A) {struct l1} : Prop :=
match l1 with
| nil => False
| b :: m => b = a0 \/ In a0 m
end) x l0 -> P x) => (fun H4 : P x => H4) (H3 H0))
(fun H2 : a = x => H1 (or_introl H2))
(fun
H2 : (fix In (a0 : A) (l1 : list A) {struct l1} : Prop :=
match l1 with
| nil => False
| b :: m => b = a0 \/ In a0 m
end) x l0 => H1 (or_intror H2))) (H x))) l).
Lemma Forall_forall1: forall {A : Type} (P : A -> Prop) (l : list A),
Forall P l -> (forall x : A, In x l -> P x).
Proof.
intros until 1.
destruct (@Forall_forall A P l).
apply H0. auto.
Defined.
Lemma Forall_cons': forall {A : Type} (P : A -> Prop) (a: A) (l : list A),
Forall P (a::l) <-> P a /\ Forall P l.
Proof.
intros ; split ; intro.
rewrite Forall_forall in H.
split.
apply H ; simpl ; auto.
rewrite Forall_forall.
intros ; apply H ; simpl ; auto.
destruct H.
apply Forall_cons ; auto.
Qed.
(*
Lemma Zcompare_refl: forall n, Z.compare n n = Eq.
Proof.
intros.
destruct n; simpl.
apply eq_refl.
unfold Pos.compare.
induction p; simpl; auto.
unfold Pos.compare.
induction p; simpl; auto.
Defined.
Lemma Zle_refl: forall n, Z.le n n.
Proof.
intros.
unfold Z.le. rewrite Zcompare_refl. intro; discriminate.
Defined.
Lemma Zle_max_l: forall n m : Z, n <= Z.max n m.
Proof.
intros.
unfold Z.max.
unfold Z.le.
destruct (n?=m) eqn:H.
rewrite Zcompare_refl; intro; discriminate.
rewrite H. intro; discriminate.
rewrite Zcompare_refl; intro; discriminate.
Defined.
Definition Pos_compare_cont_antisym :
forall (p q : positive) (c : comparison),
eq (CompOpp (Pos.compare_cont c p q))
(Pos.compare_cont (CompOpp c) q p ) :=
fun (p q : positive) (c : comparison) =>
positive_ind
(fun p0 : positive =>
forall (q0 : positive) (c0 : comparison),
CompOpp (Pos.compare_cont c0 p0 q0) =
Pos.compare_cont (CompOpp c0) q0 p0)
(fun (p0 : positive)
(IHp : forall (q0 : positive) (c0 : comparison),
CompOpp (Pos.compare_cont c0 p0 q0) =
Pos.compare_cont (CompOpp c0) q0 p0)
(q0 : positive) =>
match
q0 as p1
return
(forall c0 : comparison,
CompOpp (Pos.compare_cont c0 p0~1 p1) =
Pos.compare_cont (CompOpp c0) p1 p0~1)
with
| (q1~1)%positive =>
fun c0 : comparison => IHp q1 c0
| (q1~0)%positive =>
fun c0 : comparison => IHp q1 Gt
| 1%positive => fun c0 : comparison => eq_refl
end)
(fun (p0 : positive)
(IHp : forall (q0 : positive) (c0 : comparison),
CompOpp (Pos.compare_cont c0 p0 q0) =
Pos.compare_cont (CompOpp c0) q0 p0)
(q0 : positive) =>
match
q0 as p1
return
(forall c0 : comparison,
CompOpp (Pos.compare_cont c0 p0~0 p1) =
Pos.compare_cont (CompOpp c0) p1 p0~0)
with
| (q1~1)%positive =>
fun c0 : comparison => IHp q1 Lt
| (q1~0)%positive =>
fun c0 : comparison => IHp q1 c0
| 1%positive => fun c0 : comparison => eq_refl
end)
(fun q0 : positive =>
match
q0 as p0
return
(forall c0 : comparison,
CompOpp (Pos.compare_cont c0 1 p0) =
Pos.compare_cont (CompOpp c0) p0 1)
with
| (q1~1)%positive =>
fun c0 : comparison => eq_refl
| (q1~0)%positive =>
fun c0 : comparison => eq_refl
| 1%positive => fun c0 : comparison => eq_refl
end) p q c.
Definition Pos_compare_antisym:
forall p q : positive,
eq (Pos.compare q p) (CompOpp (Pos.compare p q)) :=
fun p q : positive =>
eq_ind_r (fun c : comparison => eq (Pos.compare_cont Eq q p) c) eq_refl
(Pos_compare_cont_antisym p q Eq).
Lemma Pos_compare_absurd:
forall x y c, (eq (Pos.compare_cont c x y) Eq) -> c=Eq.
Proof.
induction x; destruct y; simpl; intros; eauto; try discriminate.
apply IHx in H; discriminate.
apply IHx in H; discriminate.
Defined.
Lemma Pos_compare_cont_eq:
forall x y c, eq (Pos.compare_cont c x y) Eq -> eq x y.
Proof.
induction x; destruct y; simpl; intros; auto; try discriminate.
f_equal. eauto.
apply Pos_compare_absurd in H; inversion H.
apply Pos_compare_absurd in H; inversion H.
f_equal. eauto.
Defined.
Lemma Pos_compare_eq:
forall x y, eq (Pos.compare x y) Eq -> eq x y.
Proof.
intros.
apply Pos_compare_cont_eq in H; auto.
Defined.
Lemma Zmax_comm: forall n m, Z.max n m = Z.max m n.
Proof.
destruct n, m; simpl; try apply eq_refl.
*
unfold Z.max; simpl.
rename p0 into q.
rewrite Pos_compare_antisym.
destruct (Pos.compare q p) eqn:?; simpl; try reflexivity.
apply Pos_compare_eq in Heqc.
apply f_equal. symmetry; auto.
*
unfold Z.max; simpl.
rename p0 into q.
rewrite Pos_compare_antisym.
destruct (Pos.compare q p) eqn:?; simpl; try reflexivity.
apply Pos_compare_eq in Heqc.
apply f_equal. symmetry; auto.
Defined.
Lemma Zle_max_r: forall n m : Z, m <= Z.max n m.
Proof.
intros.
rewrite Z.max_comm. apply Zle_max_l.
Defined.
*)
\ No newline at end of file
......@@ -170,15 +170,21 @@ Proof.
intros m Hm.
unfold getCarry.
rewrite Z.shiftr_div_pow2 ; try omega.
SearchAbout Z.div Z.mul.
apply Z.div_pos.
assumption.
rewrite <- Z.gt_lt_iff.
apply pown0.
assert(1<= m / 2 ^ n).
replace 1 with (2 ^ n/2 ^ n) by (apply Z_div_same_full; intro ; assert(Ht:= pown0 n Hn) ; omega).
apply Z_div_le.
apply pown0 ; auto.
omega.
assert(m / 2 ^ n < 2).
apply Z.div_lt_upper_bound.
assert(Hnn := pown0 n Hn) ; omega.
rewrite Z.mul_comm.
rewrite <- Z.pow_succ_r.
destruct Hm.
rewrite <- Z.add_1_r.
assumption.
omega.
omega.
Qed.
End Integer.
\ No newline at end of file
Require Export Tools.
Require Export Forall.
Require Export notations.
Open Scope Z.
......@@ -46,7 +47,7 @@ Proof. rewrite Z.gt_lt_iff ; apply Z.pow_gt_1 ; try omega. Qed.
Lemma pown0: 2 ^ n > 0.
Proof. assert(Hp:= pown) ; omega. Qed.
Lemma ZofList_eq : forall l i, i >= 0 -> ZofListi l i = 2^(n * i) * ZofList l.
Lemma ZofList_eq : forall l i, 0 <= i -> ZofListi l i = 2^(n * i) * ZofList l.
Proof.
dependent induction l; go.
intros i Hi.
......@@ -181,6 +182,98 @@ Proof.
go.
Qed.
Lemma ZofList_le_0 : forall l, Forall (Zle 0) l -> 0 <= .lst l.
Proof.
intros l Hl.
dependent induction Hl.
- go.
- rewrite ZofList_cons.
apply OMEGA2.
assumption.
rewrite Z.mul_comm.
apply Zmult_gt_0_le_0_compat.
apply pown0.
auto.
Qed.
Lemma ZofList_null : forall l, Forall (Zle 0) l -> .lst l = 0 -> Forall (Z.eq 0) l.
Proof.
intros l HFl HSl.
induction HFl.
- go.
- assert(Hx: {x < 0} + {x = 0} + {x > 0}) by apply Ztrichotomy_inf.
assert(Hl: {.lst l < 0} + {.lst l = 0} + {.lst l > 0}) by apply Ztrichotomy_inf.
rewrite ZofList_cons in HSl.
assert(Hlpos:= ZofList_le_0 l HFl).
case Hl ; intro Hl'.
case Hl' ; intro Hl''.
apply Zle_not_lt in Hlpos.
false.
+ clear Hl' Hl Hlpos.
case Hx ; intro Hx'.
case Hx' ; intro Hx''.
apply Zle_not_lt in H.
false.
* clear Hx' Hx.
apply Forall_cons ; go.
* assert(2 ^ n * (.lst l) = 0).
rewrite Z.eq_mul_0 ; auto.
rewrite H0 in HSl.
omega.
+ clear Hlpos Hl.
case Hx ; intro Hx'.
case Hx' ; intro Hx''.
apply Zle_not_lt in H.
false.
* clear Hx' Hx.
subst x.
rewrite Z.add_0_l in HSl.
rewrite Z.eq_mul_0 in HSl.
destruct HSl.
assert(H0' := pown0) ; omega.
omega.
* assert(0 < x + 2 ^ n * (.lst l)).
apply Z.add_pos_pos.
omega.
rewrite Z.lt_0_mul.
left.
split ; rewrite <- Z.gt_lt_iff.
apply pown0.
assumption.
omega.
Qed.
Lemma ZofList_bound : forall (m:Z) l , 0 <= m < 2 ^ n -> Forall (Zle 0) l -> .lst l = m -> nth 0 l 0 = m.
Proof.
intros m l Hm HFl HSlm.
destruct l.
- go.
- rewrite ZofList_cons in HSlm.
unfold nth.
subst m.
replace (2 ^ n * (.lst l)) with 0.
apply Zplus_0_r_reverse.
rewrite Forall_cons' in HFl.
destruct HFl as [Hz Hpos].
apply ZofList_le_0 in Hpos.
assert(Hl: {.lst l < 0} + {.lst l = 0} + {.lst l > 0}) by apply Ztrichotomy_inf.
case Hl ; intro Hl'.
case Hl' ; intro Hl''.
apply Zle_not_lt in Hpos.
false.
+ symmetry. rewrite Z.eq_mul_0 ; auto.
+ exfalso.
clear Hl Hpos.
assert(1 <= .lst l).
omega.
assert(2 ^ n * 1 <= 2 ^ n * (.lst l)).
apply Zmult_le_compat_l ; auto.
rewrite <- Z.ge_le_iff.
assert(Ht:= pown0).
omega.
omega.
Qed.
End Integer.
Close Scope Z.
......
......@@ -7,8 +7,9 @@ all:
@echo generating tools and libs
${COQ} Tools.v
${COQ} notations.v
${COQ} Reduce.v
${COQ} Forall.v
${COQ} ZofList.v
${COQ} Reduce.v
${COQ} Carry.v
${COQ} SumList.v
${COQ} ScalarMult.v
......
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