Commit fcf368ba authored by Heiko Becker's avatar Heiko Becker

More additions to Exp OrderedType

parent 2ba31c82
...@@ -2,7 +2,8 @@ ...@@ -2,7 +2,8 @@
Formalization of the base expression language for the daisy framework Formalization of the base expression language for the daisy framework
**) **)
Require Import Coq.Reals.Reals Coq.micromega.Psatz Coq.QArith.QArith Require Import Coq.Reals.Reals Coq.micromega.Psatz Coq.QArith.QArith
Coq.QArith.Qreals Coq.Structures.Orders Coq.Structures.OrdersFacts. Coq.QArith.Qreals Coq.Structures.Orders Coq.Structures.OrderedType
Coq.Structures.OrdersFacts.
Require Import Daisy.Infra.RealRationalProps Daisy.Infra.RationalSimps Require Import Daisy.Infra.RealRationalProps Daisy.Infra.RationalSimps
Daisy.Infra.Ltacs. Daisy.Infra.Ltacs.
Require Export Daisy.Infra.Abbrevs Daisy.Infra.RealSimps Daisy.Infra.NatSet Require Export Daisy.Infra.Abbrevs Daisy.Infra.RealSimps Daisy.Infra.NatSet
...@@ -197,6 +198,7 @@ Module ExpOrderedType (V_ordered:OrderedType) <: OrderedType. ...@@ -197,6 +198,7 @@ Module ExpOrderedType (V_ordered:OrderedType) <: OrderedType.
Module V_orderedFacts := OrderedTypeFacts (V_ordered). Module V_orderedFacts := OrderedTypeFacts (V_ordered).
Definition V := V_ordered.t. Definition V := V_ordered.t.
Definition t := exp V.
Fixpoint expCompare (e1:exp V) (e2:exp V) := Fixpoint expCompare (e1:exp V) (e2:exp V) :=
match e1, e2 with match e1, e2 with
...@@ -635,9 +637,59 @@ Module ExpOrderedType (V_ordered:OrderedType) <: OrderedType. ...@@ -635,9 +637,59 @@ Module ExpOrderedType (V_ordered:OrderedType) <: OrderedType.
simpl in *; auto. simpl in *; auto.
Qed. Qed.
End ExpOrderedType. Instance eq_equiv: Equivalence eq.
Proof.
split; unfold Reflexive, Symmetric, Transitive, eq.
- apply expCompare_refl.
- intros. rewrite expCompare_antisym in * |-.
rewrite CompOpp_iff in * |- .
auto.
- apply expCompare_eq_trans.
Defined.
Parameter eq_dec : forall x y, { eq x y } + { ~ eq x y }.
Definition eq_refl : forall x, eq x x.
Proof.
apply expCompare_refl.
Defined.
Definition eq_sym : forall x y, eq x y -> eq y x.
Proof.
unfold eq; intros.
rewrite expCompare_antisym in * |-.
rewrite CompOpp_iff in * |-.
auto.
Defined.
Definition eq_trans : forall x y z, eq x y -> eq y z -> eq x z.
Proof.
apply expCompare_eq_trans.
Defined.
Definition lt_trans : forall x y z : t, lt x y -> lt y z -> lt x z.
Proof.
pose proof lt_strorder as [_ Trans].
apply Trans.
Defined.
(* MARKER *) Definition lt_not_eq : forall x y : t, lt x y -> ~ eq x y.
Proof.
intros. unfold lt,eq in *. hnf; intros; congruence.
Defined.
Definition compare e1 e2:= expCompare e1 e2.
(* Definition compare (e1 e2:t) :Compare lt eq e1 e2. *)
(* Proof. *)
(* destruct (expCompare e1 e2) eqn:?. *)
(* - eapply EQ. unfold eq; auto. *)
(* - eapply LT; auto. *)
(* - eapply GT. rewrite expCompare_antisym in * |-. *)
(* rewrite CompOpp_iff in *. *)
(* auto. *)
(* Defined. *)
End ExpOrderedType.
Fixpoint toRExp (e:exp Q) := Fixpoint toRExp (e:exp Q) :=
match e with match e with
......
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