Commit b3096172 authored by ='s avatar =
Browse files

Cleaning coq files

parent fc30b638
......@@ -56,6 +56,9 @@ Definition emptyEnv:env := fun _ => None.
Define environment update function as abbreviation, for variable environments
**)
Definition updEnv (x:nat) (v: R) (E:env) (y:nat) :=
if (y =? x)
if (y =? x)
then Some v
else E y.
\ No newline at end of file
else E y.
Definition updDefVars (x:nat) (m:mType) (defVars:nat -> option mType) (y:nat) :=
if (y =? x) then Some m else defVars y.
......@@ -7,7 +7,7 @@ Require Import Coq.Reals.Reals Coq.micromega.Psatz.
**)
Inductive mType: Type := M0 | M32 | M64 | M128 | M256.
Definition inj_eps_Q (e:mType) : Q :=
Definition meps (e:mType) : Q :=
match e with
| M0 => 0
| M32 => (Qpower (2#1) (Zneg 24))
......@@ -18,34 +18,32 @@ Definition inj_eps_Q (e:mType) : Q :=
| M256 => (Qpower (2#1) (Zneg 211))
end.
Definition meps := inj_eps_Q.
Lemma inj_eps_pos :
forall e, 0 <= inj_eps_Q e.
Lemma meps_pos :
forall e, 0 <= meps e.
Proof.
intro e.
case_eq e; intro; simpl inj_eps_Q; apply Qle_bool_iff; auto.
case_eq e; intro; simpl meps; apply Qle_bool_iff; auto.
Qed.
Lemma inj_eps_posR :
Lemma meps_posR :
forall e, (0 <= Q2R (meps e))%R.
Proof.
intro.
assert (Q2R 0 = 0%R) by (unfold Q2R; simpl; lra).
rewrite <- H.
apply Qle_Rle.
apply inj_eps_pos.
apply meps_pos.
Qed.
(* Definition mTypeEqBool (m1:mType) (m2:mType) := *)
(* Qeq_bool (meps m1) (meps m2). *)
(* TODO: unused? *)
Theorem eq_mType_dec: forall (m1 m2:mType), {m1 = m2} + {m1 <> m2}.
Proof.
intros.
case_eq m1; intros; case_eq m2; intros; auto; right; intro; inversion H1.
Qed.
(* Theorem eq_mType_dec: forall (m1 m2:mType), {m1 = m2} + {m1 <> m2}. *)
(* Proof. *)
(* intros. *)
(* case_eq m1; intros; case_eq m2; intros; auto; right; intro; inversion H1. *)
(* Qed. *)
Definition mTypeEqBool (m1:mType) (m2:mType) :=
match m1, m2 with
......@@ -62,7 +60,7 @@ Lemma mTypeEqBool_sym (m1:mType) (m2:mType):
Proof.
intros.
destruct b, m1, m2; simpl; cbv; auto.
Qed.
Qed.
Lemma mTypeEqBool_refl (m:mType):
mTypeEqBool m m = true.
......@@ -209,7 +207,7 @@ Proof.
assert (M0 = M0) by auto.
intros; split.
- apply (ifM0isJoin_l M0 m1 m2); auto.
- apply (ifM0isJoin_r M0 m1 m2); auto.
- apply (ifM0isJoin_r M0 m1 m2); auto.
Qed.
Lemma computeJoinIsJoin (m1:mType) (m2:mType) :
......
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