Commit 0b08dac2 authored by Raphaël Monat's avatar Raphaël Monat
Browse files

Added various lemma in MachineType.v

parent 77737f5f
......@@ -25,6 +25,16 @@ Proof.
case_eq e; intro; simpl inj_eps_Q; apply Qle_bool_iff; auto.
Qed.
Lemma inj_eps_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.
Qed.
(* Definition mTypeEqBool (m1:mType) (m2:mType) := *)
(* Qeq_bool (meps m1) (meps m2). *)
......@@ -133,7 +143,7 @@ Definition isJoinOf (m:mType) (m1:mType) (m2:mType) :=
Definition computeJoin (m1:mType) (m2:mType) :=
if (isMorePrecise m1 m2) then m1 else m2.
(* Lemma eq_compat_join (m:mType) (m2:mType) (m1:mType) (m0:mType) : *)
(* mTypeEq m m2 -> *)
......@@ -206,6 +216,18 @@ Definition computeJoin (m1:mType) (m2:mType) :=
(* (* Qed. *) *)
Lemma ifisMorePreciseM0 (m:mType) :
isMorePrecise M0 m = true -> m = M0.
Proof.
intro.
unfold isMorePrecise in H.
case_eq (mTypeEqBool m M0); intros; rewrite H0 in H; auto.
- apply EquivEqBoolEq in H0; auto.
- assert (mTypeEqBool M0 M0 = true) by (apply EquivEqBoolEq; auto).
rewrite H1 in H.
inversion H.
Qed.
Lemma ifM0isJoin_l (m:mType) (m1:mType) (m2:mType) :
m = M0 -> isJoinOf m m1 m2 = true -> m1 = M0.
Proof.
......@@ -234,3 +256,51 @@ Proof.
unfold mTypeEqBool in H0; inversion H0.
- apply EquivEqBoolEq in H; auto.
Qed.
Lemma computeJoinIsJoin (m1:mType) (m2:mType) :
isJoinOf (computeJoin m1 m2) m1 m2 = true.
Proof.
remember (computeJoin m1 m2) as m.
unfold isJoinOf.
unfold computeJoin in Heqm.
case_eq (isMorePrecise m1 m2); intros; auto;
rewrite H in Heqm;
rewrite Heqm;
apply EquivEqBoolEq; auto.
Qed.
Lemma isJoinComputeJoin (M:mType) (m1:mType) (m2:mType) :
isJoinOf M m1 m2 = true ->
M = computeJoin m1 m2.
Proof.
intros.
unfold computeJoin.
unfold isJoinOf in H.
case_eq (isMorePrecise m1 m2); intros; auto; rewrite H0 in H; apply EquivEqBoolEq; auto.
Qed.
(* Lemma joinIsMP (m1:mType) (m2:mType) : *)
(* isMorePrecise (computeJoin m1 m2) m1 = true. *)
(* Proof. *)
(* unfold computeJoin. *)
(* case_eq (isMorePrecise m1 m2); intros. *)
(* apply isMorePrecise_refl. *)
(* unfold isMorePrecise in *. *)
(* case_eq (mTypeEqBool m2 M0); intros; rewrite H0 in H; auto. *)
(* inversion H. *)
(* case_eq (mTypeEqBool m1 M0); intros; rewrite H1 in H; auto. *)
(* rewrite Qle_bool_iff. *)
(* apply Qnot_lt_le. *)
(* intro. *)
(* apply not_true_iff_false in H. *)
(* Lemma Qnot_lt_le : forall x y, ~ x<y -> y<=x. *)
(* Lemma Qnot_le_lt : forall x y, ~ x<=y -> y<x. *)
(* Lemma Qlt_not_le : forall x y, x<y -> ~ y<=x. *)
(* Lemma Qle_not_lt : forall x y, x<=y -> ~ y<x. *)
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