Commit 4325b20b authored by Guillaume Melquiond's avatar Guillaume Melquiond

Update Coq realizations.

parent 378da39d
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below *)
Require Import ZArith.
Require Import Rbase.
Require Import BuiltIn.
Require BuiltIn.
(* Why3 goal *)
Notation infix_ls := Zlt (only parsing).
......@@ -26,41 +26,68 @@ Notation prefix_mn := Zopp (only parsing).
(* Why3 goal *)
Notation infix_as := Zmult (only parsing).
(* Why3 goal *)
Lemma Unit_def : forall (x:Z), ((infix_pl x 0%Z) = x).
exact Zplus_0_r.
Qed.
(* Why3 goal *)
Lemma Assoc : forall (x:Z) (y:Z) (z:Z), ((infix_pl (infix_pl x y)
z) = (infix_pl x (infix_pl y z))).
Proof.
intros x y z.
apply sym_eq.
apply Zplus_assoc.
Qed.
(* Why3 goal *)
Lemma Inv_def : forall (x:Z), ((infix_pl x (prefix_mn x)) = 0%Z).
Lemma Unit_def_l : forall (x:Z), ((infix_pl 0%Z x) = x).
Proof.
exact Zplus_0_l.
Qed.
(* Why3 goal *)
Lemma Unit_def_r : forall (x:Z), ((infix_pl x 0%Z) = x).
Proof.
exact Zplus_0_r.
Qed.
(* Why3 goal *)
Lemma Inv_def_l : forall (x:Z), ((infix_pl (prefix_mn x) x) = 0%Z).
Proof.
exact Zplus_opp_l.
Qed.
(* Why3 goal *)
Lemma Inv_def_r : forall (x:Z), ((infix_pl x (prefix_mn x)) = 0%Z).
Proof.
exact Zplus_opp_r.
Qed.
(* Why3 goal *)
Lemma Comm : forall (x:Z) (y:Z), ((infix_pl x y) = (infix_pl y x)).
Proof.
exact Zplus_comm.
Qed.
(* Why3 goal *)
Lemma Assoc1 : forall (x:Z) (y:Z) (z:Z), ((infix_as (infix_as x y)
z) = (infix_as x (infix_as y z))).
Proof.
intros x y z.
apply sym_eq.
apply Zmult_assoc.
Qed.
(* Why3 goal *)
Lemma Mul_distr : forall (x:Z) (y:Z) (z:Z), ((infix_as x (infix_pl y
Lemma Mul_distr_l : forall (x:Z) (y:Z) (z:Z), ((infix_as x (infix_pl y
z)) = (infix_pl (infix_as x y) (infix_as x z))).
exact Zmult_plus_distr_r.
Proof.
intros x y z.
apply Zmult_plus_distr_r.
Qed.
(* Why3 goal *)
Lemma Mul_distr_r : forall (x:Z) (y:Z) (z:Z), ((infix_as (infix_pl y z)
x) = (infix_pl (infix_as y x) (infix_as z x))).
Proof.
intros x y z.
apply Zmult_plus_distr_l.
Qed.
(* Why3 assumption *)
......@@ -68,21 +95,25 @@ Definition infix_mn(x:Z) (y:Z): Z := (infix_pl x (prefix_mn y)).
(* Why3 goal *)
Lemma Comm1 : forall (x:Z) (y:Z), ((infix_as x y) = (infix_as y x)).
Proof.
exact Zmult_comm.
Qed.
(* Why3 goal *)
Lemma Unitary : forall (x:Z), ((infix_as 1%Z x) = x).
Proof.
exact Zmult_1_l.
Qed.
(* Why3 goal *)
Lemma NonTrivialRing : ~ (0%Z = 1%Z).
Proof.
discriminate.
Qed.
(* Why3 goal *)
Lemma Refl : forall (x:Z), (infix_lseq x x).
Proof.
intros x.
apply infix_lseq_Zle.
apply Zle_refl.
......@@ -91,6 +122,7 @@ Qed.
(* Why3 goal *)
Lemma Trans : forall (x:Z) (y:Z) (z:Z), (infix_lseq x y) -> ((infix_lseq y
z) -> (infix_lseq x z)).
Proof.
intros x y z H1 H2.
apply infix_lseq_Zle.
apply Zle_trans with y ;
......@@ -100,6 +132,7 @@ Qed.
(* Why3 goal *)
Lemma Antisymm : forall (x:Z) (y:Z), (infix_lseq x y) -> ((infix_lseq y x) ->
(x = y)).
Proof.
intros x y H1 H2.
apply Zle_antisym ;
now apply infix_lseq_Zle.
......@@ -107,6 +140,7 @@ Qed.
(* Why3 goal *)
Lemma Total : forall (x:Z) (y:Z), (infix_lseq x y) \/ (infix_lseq y x).
Proof.
intros x y.
destruct (Zle_or_lt x y) as [H|H].
left.
......@@ -118,12 +152,14 @@ Qed.
(* Why3 goal *)
Lemma ZeroLessOne : (infix_lseq 0%Z 1%Z).
Proof.
now left.
Qed.
(* Why3 goal *)
Lemma CompatOrderAdd : forall (x:Z) (y:Z) (z:Z), (infix_lseq x y) ->
(infix_lseq (infix_pl x z) (infix_pl y z)).
Proof.
intros x y z H.
apply infix_lseq_Zle.
apply Zplus_le_compat_r.
......@@ -133,6 +169,7 @@ Qed.
(* Why3 goal *)
Lemma CompatOrderMult : forall (x:Z) (y:Z) (z:Z), (infix_lseq x y) ->
((infix_lseq 0%Z z) -> (infix_lseq (infix_as x z) (infix_as y z))).
Proof.
intros x y z H1 H2.
apply infix_lseq_Zle.
apply Zmult_le_compat_r ;
......
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below *)
Require Import ZArith.
Require Import Rbase.
Require Import BuiltIn.
Require BuiltIn.
(* Why3 goal *)
Definition infix_ls: R -> R -> Prop.
......@@ -27,36 +27,63 @@ exact Rmult.
Defined.
(* Why3 goal *)
Lemma Unit_def : forall (x:R), ((infix_pl x 0%R) = x).
Lemma Assoc : forall (x:R) (y:R) (z:R), ((infix_pl (infix_pl x y)
z) = (infix_pl x (infix_pl y z))).
Proof.
exact Rplus_assoc.
Qed.
(* Why3 goal *)
Lemma Unit_def_l : forall (x:R), ((infix_pl 0%R x) = x).
Proof.
exact Rplus_0_l.
Qed.
(* Why3 goal *)
Lemma Unit_def_r : forall (x:R), ((infix_pl x 0%R) = x).
Proof.
exact Rplus_0_r.
Qed.
(* Why3 goal *)
Lemma Assoc : forall (x:R) (y:R) (z:R), ((infix_pl (infix_pl x y)
z) = (infix_pl x (infix_pl y z))).
exact Rplus_assoc.
Lemma Inv_def_l : forall (x:R), ((infix_pl (prefix_mn x) x) = 0%R).
Proof.
exact Rplus_opp_l.
Qed.
(* Why3 goal *)
Lemma Inv_def : forall (x:R), ((infix_pl x (prefix_mn x)) = 0%R).
Lemma Inv_def_r : forall (x:R), ((infix_pl x (prefix_mn x)) = 0%R).
Proof.
exact Rplus_opp_r.
Qed.
(* Why3 goal *)
Lemma Comm : forall (x:R) (y:R), ((infix_pl x y) = (infix_pl y x)).
Proof.
exact Rplus_comm.
Qed.
(* Why3 goal *)
Lemma Assoc1 : forall (x:R) (y:R) (z:R), ((infix_as (infix_as x y)
z) = (infix_as x (infix_as y z))).
Proof.
exact Rmult_assoc.
Qed.
(* Why3 goal *)
Lemma Mul_distr : forall (x:R) (y:R) (z:R), ((infix_as x (infix_pl y
Lemma Mul_distr_l : forall (x:R) (y:R) (z:R), ((infix_as x (infix_pl y
z)) = (infix_pl (infix_as x y) (infix_as x z))).
exact Rmult_plus_distr_l.
Proof.
intros x y z.
apply Rmult_plus_distr_l.
Qed.
(* Why3 goal *)
Lemma Mul_distr_r : forall (x:R) (y:R) (z:R), ((infix_as (infix_pl y z)
x) = (infix_pl (infix_as y x) (infix_as z x))).
Proof.
intros x y z.
apply Rmult_plus_distr_r.
Qed.
(* Why3 assumption *)
......@@ -64,16 +91,19 @@ Definition infix_mn(x:R) (y:R): R := (infix_pl x (prefix_mn y)).
(* Why3 goal *)
Lemma Comm1 : forall (x:R) (y:R), ((infix_as x y) = (infix_as y x)).
Proof.
exact Rmult_comm.
Qed.
(* Why3 goal *)
Lemma Unitary : forall (x:R), ((infix_as 1%R x) = x).
Proof.
exact Rmult_1_l.
Qed.
(* Why3 goal *)
Lemma NonTrivialRing : ~ (0%R = 1%R).
Proof.
apply not_eq_sym.
exact R1_neq_R0.
Qed.
......@@ -94,6 +124,7 @@ Definition infix_sl(x:R) (y:R): R := (infix_as x (inv y)).
(* Why3 goal *)
Lemma add_div : forall (x:R) (y:R) (z:R), (~ (z = 0%R)) ->
((infix_sl (infix_pl x y) z) = (infix_pl (infix_sl x z) (infix_sl y z))).
Proof.
intros.
unfold infix_sl, infix_as, infix_pl.
field.
......@@ -102,6 +133,7 @@ Qed.
(* Why3 goal *)
Lemma sub_div : forall (x:R) (y:R) (z:R), (~ (z = 0%R)) ->
((infix_sl (infix_mn x y) z) = (infix_mn (infix_sl x z) (infix_sl y z))).
Proof.
intros.
unfold infix_sl, infix_as, infix_mn, infix_pl, prefix_mn.
field.
......@@ -110,6 +142,7 @@ Qed.
(* Why3 goal *)
Lemma neg_div : forall (x:R) (y:R), (~ (y = 0%R)) -> ((infix_sl (prefix_mn x)
y) = (prefix_mn (infix_sl x y))).
Proof.
intros.
unfold infix_sl, infix_as, prefix_mn.
field.
......@@ -118,6 +151,7 @@ Qed.
(* Why3 goal *)
Lemma assoc_mul_div : forall (x:R) (y:R) (z:R), (~ (z = 0%R)) ->
((infix_sl (infix_as x y) z) = (infix_as x (infix_sl y z))).
Proof.
intros x y z _.
apply Rmult_assoc.
Qed.
......@@ -126,6 +160,7 @@ Qed.
Lemma assoc_div_mul : forall (x:R) (y:R) (z:R), ((~ (y = 0%R)) /\
~ (z = 0%R)) -> ((infix_sl (infix_sl x y) z) = (infix_sl x (infix_as y
z))).
Proof.
intros x y z (Zy, Zz).
unfold infix_sl, infix_as, inv.
rewrite Rmult_assoc.
......@@ -136,6 +171,7 @@ Qed.
Lemma assoc_div_div : forall (x:R) (y:R) (z:R), ((~ (y = 0%R)) /\
~ (z = 0%R)) -> ((infix_sl x (infix_sl y z)) = (infix_sl (infix_as x z)
y)).
Proof.
intros x y z (Zy, Zz).
unfold infix_sl, infix_as, inv.
field.
......@@ -144,23 +180,27 @@ Qed.
(* Why3 goal *)
Lemma Refl : forall (x:R), (infix_lseq x x).
Proof.
exact Rle_refl.
Qed.
(* Why3 goal *)
Lemma Trans : forall (x:R) (y:R) (z:R), (infix_lseq x y) -> ((infix_lseq y
z) -> (infix_lseq x z)).
Proof.
exact Rle_trans.
Qed.
(* Why3 goal *)
Lemma Antisymm : forall (x:R) (y:R), (infix_lseq x y) -> ((infix_lseq y x) ->
(x = y)).
Proof.
exact Rle_antisym.
Qed.
(* Why3 goal *)
Lemma Total : forall (x:R) (y:R), (infix_lseq x y) \/ (infix_lseq y x).
Proof.
intros x y.
destruct (Rle_or_lt x y) as [H|H].
now left.
......@@ -170,12 +210,14 @@ Qed.
(* Why3 goal *)
Lemma ZeroLessOne : (infix_lseq 0%R 1%R).
Proof.
exact Rle_0_1.
Qed.
(* Why3 goal *)
Lemma CompatOrderAdd : forall (x:R) (y:R) (z:R), (infix_lseq x y) ->
(infix_lseq (infix_pl x z) (infix_pl y z)).
Proof.
intros x y z.
exact (Rplus_le_compat_r z x y).
Qed.
......@@ -183,6 +225,7 @@ Qed.
(* Why3 goal *)
Lemma CompatOrderMult : forall (x:R) (y:R) (z:R), (infix_lseq x y) ->
((infix_lseq 0%R z) -> (infix_lseq (infix_as x z) (infix_as y z))).
Proof.
intros x y z H Zz.
now apply Rmult_le_compat_r.
Qed.
......
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