Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Adapt the various "Let" ended with Qed #82

Merged
merged 1 commit into from
Oct 30, 2023
Merged

Adapt the various "Let" ended with Qed #82

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
6 changes: 3 additions & 3 deletions BigN/BigN.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -177,7 +177,7 @@ Add Ring BigNr : BigNring
Section TestRing.
Let test : forall x y, 1 + x*y^1 + x^2 + 1 == 1*1 + 1 + y*x + 1*x*x.
intros. ring_simplify. reflexivity.
Qed.
Defined.
End TestRing.

(** We benefit also from an "order" tactic *)
Expand All @@ -186,12 +186,12 @@ Ltac bigN_order := BigN.order.

Section TestOrder.
Let test : forall x y : bigN, x<=y -> y<=x -> x==y.
Proof. bigN_order. Qed.
Proof. bigN_order. Defined.
End TestOrder.

(** We can use at least a bit of lia by translating to [Z]. *)

Section TestLia.
Let test : forall x y : bigN, x<=y -> y<=x -> x==y.
Proof. intros x y. BigN.zify. lia. Qed.
Proof. intros x y. BigN.zify. lia. Defined.
End TestLia.
2 changes: 1 addition & 1 deletion BigN/NMake.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -247,7 +247,7 @@ Module Make (W0:CyclicType) <: NType.
let compare0 := compare zero in
fun m => compare_mn_1 (dom_t n) (dom_t n) zero compare compare0 compare (S m).

Let spec_comparen_m:
Local Lemma spec_comparen_m:
forall n m (x : word (dom_t n) (S m)) (y : dom_t n),
comparen_m n m x y = Z.compare (eval n (S m) x) (ZnZ.to_Z y).
Proof.
Expand Down
22 changes: 13 additions & 9 deletions BigN/gen/NMake_gen.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -305,7 +305,7 @@ pr "
do_size (destruct n; auto with *). apply wn_spec.
Qed.

Let make_op_WW : forall n x y,
Local Lemma make_op_WW : forall n x y,
(ZnZ.to_Z (Ops:=make_op (S n)) (WW x y) =
ZnZ.to_Z (Ops:=make_op n) x * base (ZnZ.digits (make_op n))
+ ZnZ.to_Z (Ops:=make_op n) y)%%Z.
Expand Down Expand Up @@ -601,7 +601,7 @@ pr

(** Misc results about extensions *)

Let spec_extend_WW : forall n x,
Local Lemma spec_extend_WW : forall n x,
[Nn (S n) (WW W0 x)] = [Nn n x].
Proof.
intros n x.
Expand All @@ -611,23 +611,23 @@ pr
solve_eval.
Qed.

Let spec_extend_tr: forall m n w,
Local Lemma spec_extend_tr: forall m n w,
[Nn (m + n) (extend_tr w m)] = [Nn n w].
Proof.
induction m; auto.
intros n x; simpl extend_tr.
simpl plus; rewrite spec_extend_WW; auto.
Qed.

Let spec_cast_l: forall n m x1,
Local Lemma spec_cast_l: forall n m x1,
[Nn n x1] =
[Nn (Nat.max n m) (castm (diff_r n m) (extend_tr x1 (snd (diff n m))))].
Proof.
intros n m x1; case (diff_r n m); simpl castm.
rewrite spec_extend_tr; auto.
Qed.

Let spec_cast_r: forall n m x1,
Local Lemma spec_cast_r: forall n m x1,
[Nn m x1] =
[Nn (Nat.max n m) (castm (diff_l n m) (extend_tr x1 (fst (diff n m))))].
Proof.
Expand Down Expand Up @@ -661,11 +661,12 @@ done;
pr
" Let fn n := f (SizePlus (S n)).

#[clearbody]
Let Pf' :
forall n x y u v, u = [mk_t n x] -> v = [mk_t n y] -> P u v (f n x y).
Proof.
intros. subst. rewrite 2 spec_mk_t. apply Pf.
Qed.
Defined.
";

let ext i j s =
Expand Down Expand Up @@ -753,23 +754,26 @@ pr
Variable fnm: forall n m, word (dom_t Size) (S n) -> word (dom_t Size) (S m) -> res.
Variable Pfnm: forall n m x y, P [Nn n x] [Nn m y] (fnm n m x y).

#[clearbody]
Let Pf' :
forall n x y u v, u = [mk_t n x] -> v = [mk_t n y] -> P u v (f n x y).
Proof.
intros. subst. rewrite 2 spec_mk_t. apply Pf.
Qed.
Defined.

#[clearbody]
Let Pfd' : forall n m x y u v, u = [mk_t n x] -> v = eval n (S m) y ->
P u v (fd n m x y).
Proof.
intros. subst. rewrite spec_mk_t. apply Pfd.
Qed.
Defined.

#[clearbody]
Let Pfg' : forall n m x y u v, u = eval n (S m) x -> v = [mk_t n y] ->
P u v (fg n m x y).
Proof.
intros. subst. rewrite spec_mk_t. apply Pfg.
Qed.
Defined.
";

for i = 0 to size do
Expand Down
13 changes: 8 additions & 5 deletions BigQ/BigQ.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -142,21 +142,24 @@ Add Field BigQfield : BigQfieldth

Section TestField.

#[clearbody]
Let ex1 : forall x y z, (x+y)*z == (x*z)+(y*z).
intros.
ring.
Qed.
Defined.

#[clearbody]
Let ex8 : forall x, x ^ 2 == x*x.
intro.
ring.
Qed.
Defined.

#[clearbody]
Let ex10 : forall x y, y!=0 -> (x/y)*y == x.
intros.
field.
auto.
Qed.
Defined.

End TestField.

Expand All @@ -166,13 +169,13 @@ Ltac bigQ_order := BigQ.order.

Section TestOrder.
Let test : forall x y : bigQ, x<=y -> y<=x -> x==y.
Proof. bigQ_order. Qed.
Proof. bigQ_order. Defined.
End TestOrder.

(** We can also reason by switching to QArith thanks to tactic
BigQ.qify. *)

Section TestQify.
Let test : forall x : bigQ, 0+x == 1*x.
Proof. intro x. BigQ.qify. ring. Qed.
Proof. intro x. BigQ.qify. ring. Defined.
End TestQify.
10 changes: 6 additions & 4 deletions BigZ/BigZ.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -181,14 +181,16 @@ Add Ring BigZr : BigZring
div BigZdiv).

Section TestRing.
#[clearbody]
Let test : forall x y, 1 + x*y + x^2 + 1 == 1*1 + 1 + (y + 1*x)*x.
Proof.
intros. ring_simplify. reflexivity.
Qed.
Defined.
#[clearbody]
Let test' : forall x y, 1 + x*y + x^2 - 1*1 - y*x + 1*(-x)*x == 0.
Proof.
intros. ring_simplify. reflexivity.
Qed.
Defined.
End TestRing.

(** [BigZ] also benefits from an "order" tactic *)
Expand All @@ -197,12 +199,12 @@ Ltac bigZ_order := BigZ.order.

Section TestOrder.
Let test : forall x y : bigZ, x<=y -> y<=x -> x==y.
Proof. bigZ_order. Qed.
Proof. bigZ_order. Defined.
End TestOrder.

(** We can use at least a bit of lia by translating to [Z]. *)

Section TestLia.
Let test : forall x y : bigZ, x<=y -> y<=x -> x==y.
Proof. intros x y. BigZ.zify. Lia.lia. Qed.
Proof. intros x y. BigZ.zify. Lia.lia. Defined.
End TestLia.
Loading
Loading