Commit 867f7f59 authored by Andrew Hirsch's avatar Andrew Hirsch
Browse files

Updated names of many things.

- Concurrent Lambda became Control Language
- Choreographies became Pirouette
- Expressions became Local Language

These reflect the names in the paper.
parent 8caf0587
This diff is collapsed.
Require Export Expression.
Require Export LocalLang.
Require Import Coq.Arith.PeanoNat.
Require Import Coq.Lists.List.
Module LambdaCalc <: Expression.
Module LambdaCalc <: LocalLang.
Inductive SimpleType : Set :=
boolType : SimpleType
......@@ -31,27 +31,27 @@ Module LambdaCalc <: Expression.
Qed.
Definition ExprVar : nat -> Expr := var.
Fixpoint LCClosedBelow (n : nat) (e : LC) : Prop :=
Fixpoint LCClosedAbove (n : nat) (e : LC) : Prop :=
match e with
| var m => if m <? n then True else False
| ttLC => True
| ffLC => True
| zero => True
| succ e' => LCClosedBelow n e'
| fixP e' => LCClosedBelow n e'
| ite b e1 e2 => LCClosedBelow n b /\ LCClosedBelow n e1 /\ LCClosedBelow n e2
| app e1 e2 => LCClosedBelow n e1 /\ LCClosedBelow n e2
| abs τ e' => LCClosedBelow (S n) e'
| succ e' => LCClosedAbove n e'
| fixP e' => LCClosedAbove n e'
| ite b e1 e2 => LCClosedAbove n b /\ LCClosedAbove n e1 /\ LCClosedAbove n e2
| app e1 e2 => LCClosedAbove n e1 /\ LCClosedAbove n e2
| abs τ e' => LCClosedAbove (S n) e'
end.
Definition ExprClosedBelow := LCClosedBelow.
Definition ExprClosed := ExprClosedBelow 0.
Definition ExprClosedAbove := LCClosedAbove.
Definition ExprClosed := ExprClosedAbove 0.
Inductive LCVal : LC -> Prop :=
| ttVal : LCVal ttLC
| ffVal : LCVal ffLC
| zeroVal : LCVal zero
| succVal : forall e : Expr, LCVal e -> LCVal (succ e)
| AbsVal : forall (τ : SimpleType) (e : LC), LCClosedBelow 1 e -> LCVal (abs τ e).
| AbsVal : forall (τ : SimpleType) (e : LC), LCClosedAbove 1 e -> LCVal (abs τ e).
Definition ExprVal := LCVal.
(* Inductive LCOpenVal : LC -> Prop := *)
......@@ -259,8 +259,8 @@ Module LambdaCalc <: Expression.
Global Hint Constructors LCStep : LC.
Definition ExprStep := LCStep.
Theorem ExprClosedBelowSubst : forall (e : Expr) (σ : nat -> Expr) (n : nat),
ExprClosedBelow n e -> (forall m, m < n -> σ m = ExprVar m) -> e [e|σ] = e.
Theorem ExprClosedAboveSubst : forall (e : Expr) (σ : nat -> Expr) (n : nat),
ExprClosedAbove n e -> (forall m, m < n -> σ m = ExprVar m) -> e [e|σ] = e.
Proof using.
intros e; induction e; intros σ m closed_b static_above; cbn in *; auto.
- destruct m;
......@@ -279,12 +279,12 @@ Module LambdaCalc <: Expression.
Qed.
Lemma ExprClosedSubst : forall (e : Expr) (σ : nat -> Expr), ExprClosed e -> e [e|σ] = e.
Proof using.
intros e σ closed; unfold ExprClosed in closed; apply ExprClosedBelowSubst with (n := 0);
intros e σ closed; unfold ExprClosed in closed; apply ExprClosedAboveSubst with (n := 0);
auto.
intros m lt; inversion lt.
Qed.
Theorem ExprClosedBelowMono : forall m n e, m < n -> ExprClosedBelow m e -> ExprClosedBelow n e.
Theorem ExprClosedAboveMono : forall m n e, m < n -> ExprClosedAbove m e -> ExprClosedAbove n e.
Proof using.
intros m n e; revert m n; induction e; intros k m l H; cbn in *; auto.
destruct k. destruct H. destruct (n <=? k) eqn:eq.
......@@ -300,20 +300,20 @@ Module LambdaCalc <: Expression.
apply Lt.lt_le_S in l. apply Lt.le_lt_or_eq in l; destruct l; subst; eauto.
Qed.
Fixpoint IsClosedBelow (e : Expr) (n : nat) : bool :=
Fixpoint IsClosedAbove (e : Expr) (n : nat) : bool :=
match e with
| var m => if m <? n then true else false
| ttLC => true
| ffLC => true
| zero => true
| succ e' => IsClosedBelow e' n
| fixP e' => IsClosedBelow e' n
| ite b e1 e2 => IsClosedBelow b n && IsClosedBelow e1 n && IsClosedBelow e2 n
| app e1 e2 => IsClosedBelow e1 n && IsClosedBelow e2 n
| abs τ e' => IsClosedBelow e' (S n)
| succ e' => IsClosedAbove e' n
| fixP e' => IsClosedAbove e' n
| ite b e1 e2 => IsClosedAbove b n && IsClosedAbove e1 n && IsClosedAbove e2 n
| app e1 e2 => IsClosedAbove e1 n && IsClosedAbove e2 n
| abs τ e' => IsClosedAbove e' (S n)
end.
Lemma IsClosedBelowSpec : forall e n, IsClosedBelow e n = true <-> LCClosedBelow n e.
Lemma IsClosedAboveSpec : forall e n, IsClosedAbove e n = true <-> LCClosedAbove n e.
Proof using.
intro e; induction e; intro m; cbn; split; intro H; auto; try discriminate.
1,2: destruct m; cbn in *;
......@@ -326,11 +326,11 @@ Module LambdaCalc <: Expression.
| [ |- andb _ _ = true ] => apply andb_true_intro
| [ H : _ /\ _ |- _ ] => destruct H
| [|- _ /\ _ ] => split
| [IH : forall n, IsClosedBelow ?e n = true <-> LCClosedBelow n ?e,
H : IsClosedBelow ?e ?m = true |- LCClosedBelow ?m ?e ] =>
| [IH : forall n, IsClosedAbove ?e n = true <-> LCClosedAbove n ?e,
H : IsClosedAbove ?e ?m = true |- LCClosedAbove ?m ?e ] =>
apply ((proj1 (IH m)) H)
| [IH : forall n, IsClosedBelow ?e n = true <-> LCClosedBelow n ?e,
H : LCClosedBelow ?m ?e |- IsClosedBelow ?e ?m = true ] =>
| [IH : forall n, IsClosedAbove ?e n = true <-> LCClosedAbove n ?e,
H : LCClosedAbove ?m ?e |- IsClosedAbove ?e ?m = true ] =>
apply ((proj2 (IH m)) H)
end.
Qed.
......@@ -345,18 +345,18 @@ Module LambdaCalc <: Expression.
| fixP e => false
| ite e1 e2 e3 => false
| app e1 e2 => false
| abs τ e1 => IsClosedBelow e1 1
| abs τ e1 => IsClosedAbove e1 1
end.
Lemma IsExprValSpec1 : forall v : Expr, ExprVal v -> IsExprVal v = true.
Proof using.
intros v val; induction val; cbn; auto.
apply IsClosedBelowSpec; auto.
apply IsClosedAboveSpec; auto.
Qed.
Lemma IsExprValSpec2 : forall v : Expr, IsExprVal v = true -> ExprVal v.
Proof using.
intros v eq; induction v; cbn in *; try discriminate; constructor; auto.
apply IHv; auto. apply IsClosedBelowSpec; auto.
apply IHv; auto. apply IsClosedAboveSpec; auto.
Qed.
Lemma IsExprValSpec3 : forall e : Expr, ~ ExprVal e -> IsExprVal e = false.
Proof using.
......@@ -437,10 +437,10 @@ Module LambdaCalc <: Expression.
(* - inversion H; subst. apply IHe in H1; auto. *)
(* Qed. *)
Lemma ExprRenameClosedBelow : forall e n ξ m,
Lemma ExprRenameClosedAbove : forall e n ξ m,
(forall k, k < n -> ξ k < m) ->
ExprClosedBelow n e ->
ExprClosedBelow m (e e| ξ⟩).
ExprClosedAbove n e ->
ExprClosedAbove m (e e| ξ⟩).
Proof using.
intros e; induction e; cbn; try rename n into x; intros n ξ m ξ_bdd clsd_e; auto.
all: repeat match goal with
......@@ -463,10 +463,10 @@ Module LambdaCalc <: Expression.
apply Lt.lt_n_S. apply Lt.lt_S_n in k_lt_Sn. apply ξ_bdd; auto.
Qed.
Lemma ExprSubstClosedBelow : forall e n σ m,
(forall k, k < n -> ExprClosedBelow m (σ k)) ->
ExprClosedBelow n e ->
ExprClosedBelow m (e [e| σ]).
Lemma ExprSubstClosedAbove : forall e n σ m,
(forall k, k < n -> ExprClosedAbove m (σ k)) ->
ExprClosedAbove n e ->
ExprClosedAbove m (e [e| σ]).
Proof using.
intros e; induction e; cbn; try rename n into x; intros n σ m σ_clsd e_clsd; auto;
repeat match goal with
......@@ -482,27 +482,27 @@ Module LambdaCalc <: Expression.
apply σ_clsd in H; auto.
- apply IHe with (n := S n); auto.
intros k k_lt_Sn; unfold ExprUpSubst; destruct k; cbn; auto.
apply ExprRenameClosedBelow with (n := m).
apply ExprRenameClosedAbove with (n := m).
intros l lt_l_m; apply Lt.lt_n_S; auto.
apply σ_clsd; apply Lt.lt_S_n; auto.
Qed.
Theorem ExprClosedAfterStep : forall e1 e2 n,
ExprStep e1 e2 -> ExprClosedBelow n e1 -> ExprClosedBelow n e2.
ExprStep e1 e2 -> ExprClosedAbove n e1 -> ExprClosedAbove n e2.
Proof using.
intros e1 e2 n step; revert n; induction step; cbn; intros n clsd; auto;
repeat match goal with
| [ H : _ /\ _ |- _ ] => destruct H
| [ |- _ /\ _ ] => split
end; auto.
apply ExprSubstClosedBelow with (n := S n); auto.
apply ExprSubstClosedAbove with (n := S n); auto.
intros k lt_k_Sn; unfold LCStepSubst. destruct k; auto; cbn.
destruct n. apply Lt.lt_S_n in lt_k_Sn; inversion lt_k_Sn.
apply Lt.lt_S_n in lt_k_Sn.
apply Lt.lt_n_Sm_le in lt_k_Sn. apply Nat.leb_le in lt_k_Sn; rewrite lt_k_Sn; auto.
Qed.
Theorem ExprVarClosed : forall n m, ExprClosedBelow n (ExprVar m) <-> m < n.
Theorem ExprVarClosed : forall n m, ExprClosedAbove n (ExprVar m) <-> m < n.
intros n m; cbn; split; intro H; destruct n; auto. destruct H.
destruct (m <=? n) eqn:eq. apply Nat.leb_le in eq; unfold lt; apply Le.le_n_S; auto.
destruct H.
......
Module Type Expression.
(*
Module type for the local language.
We can instantiate this module type with any
number of languages, as we can see in the examples.
*)
Module Type LocalLang.
(*
The local language is an expression-based language.
We assume that expressions have decidable syntactic equality.
This is a pretty weak assumption for syntax.
*)
Parameter Expr : Set.
Parameter ExprEqDec : forall e1 e2 : Expr, {e1 = e2} + {e1 <> e2}.
(* Since we use de Bruijn indices, we represent variables as
natural numbers. We don't require any sort of binders in
the local language, so these don't necessarily count to
the relevant binder. However, in our examples they do. *)
Parameter ExprVar : nat -> Expr.
(* An expression is closed above `n` if variables above `n`
do not appear free in the expression. Clearly, if
an expression is closed above `0`, then it contains
no free variables.
The property of being closed above is monotonic.
Moreover, variables are always closed above
anything greater than themselves.
*)
Parameter ExprClosedAbove : nat -> Expr -> Prop.
Definition ExprClosed := ExprClosedAbove 0.
Parameter ExprClosedAboveMono : forall m n e, m < n -> ExprClosedAbove m e -> ExprClosedAbove n e.
Parameter ExprVarClosed : forall n m, ExprClosedAbove n (ExprVar m) <-> m < n.
(*
Values are a subset of expressions (here represented
as a property of expressions. These are always closed.
This restriction is necessary for communication to
typecheck in Pirouette.
*)
Parameter ExprVal : Expr -> Prop.
Parameter ExprClosedBelow : nat -> Expr -> Prop.
Definition ExprClosed := ExprClosedBelow 0.
Parameter ExprValuesClosed : forall v : Expr, ExprVal v -> ExprClosed v.
Parameter ExprClosedBelowMono : forall m n e, m < n -> ExprClosedBelow m e -> ExprClosedBelow n e.
Parameter ExprVarClosed : forall n m, ExprClosedBelow n (ExprVar m) <-> m < n.
(* Parameter IsExprVal : Expr -> bool. *)
(* Parameter IsExprValSpec1 : forall v : Expr, ExprVal v -> IsExprVal v = true. *)
(* Parameter IsExprValSpec2 : forall v : Expr, IsExprVal v = true -> ExprVal v. *)
(* Lemma IsExprValSpec3 : forall e : Expr, ~ ExprVal e -> IsExprVal e = false. *)
(* Proof using. *)
(* intros e nv; destruct (IsExprVal e) eqn:eq; auto. *)
(* apply IsExprValSpec2 in eq; exfalso; apply nv; auto. *)
(* Qed. *)
(* Lemma IsExprValSpec4 : forall e : Expr, IsExprVal e = false -> ~ ExprVal e. *)
(* Proof using. *)
(* intros e eq val; apply IsExprValSpec1 in val; rewrite val in eq; inversion eq. *)
(* Qed. *)
(*
Local languages need to define a(n infinite)
substitution operator. This replaces all variables
in the expression with new subexpressions. We also
consider a renaming operation, which allows us to
substitute variables more easily with other variables.
This can be defined via the "specification" equation
below, but it is often better to define it seperately.
*)
Parameter ExprSubst : Expr -> (nat -> Expr) -> Expr.
Parameter ExprRename : Expr -> (nat -> nat) -> Expr.
Notation "e [e| sigma ]" := (ExprSubst e sigma) (at level 29).
Notation "e ⟨e| xi ⟩" := (ExprRename e xi) (at level 29).
Parameter ExprRenameSpec : forall (e : Expr) (ξ : nat -> nat),
e e| ξ⟩ = e [e| fun n => ExprVar (ξ n)].
(* Substitution must correctly replace a variable.
This allows us to show that renaming must do the same thing.
*)
Parameter ExprSubstVar : forall n σ, (ExprVar n ) [e| σ] = σ n.
Lemma ExprRenameVar : forall n ξ, (ExprVar n) e| ξ = ExprVar (ξ n).
Proof.
......@@ -36,11 +70,60 @@ Module Type Expression.
rewrite ExprRenameSpec. rewrite ExprSubstVar. reflexivity.
Qed.
(* Renaming in an expression twice should behave
compositionally. For technical reasons, we need
this to prove an important property of Pirouette. *)
Parameter ExprRenameFusion : forall (e : Expr) (ξ1 ξ2 : nat -> nat),
(e e| ξ1) e| ξ2 = e e| fun n => ξ2 (ξ1 n).
Parameter ExprSubstFusion : forall (e : Expr) (σ1 σ2 : nat -> Expr),
(e [e| σ1]) [e|σ2] = e [e| fun n => σ1 n [e| σ2]].
(* Parameter ExprSubstFusion : forall (e : Expr) (σ1 σ2 : nat -> Expr), *)
(* (e [e| σ1]) [e|σ2] = e [e| fun n => σ1 n [e| σ2]]. *)
(*
Substitution must be _extensional_ in the sense
that it does not rely on the implementation of
the substitution functions. This allows us to show
that renaming is also extensional.
*)
Parameter ExprSubstExt : forall (e : Expr) (σ1 σ2 : nat -> Expr),
(forall n, σ1 n = σ2 n) -> e [e| σ1] = e [e| σ2].
Lemma ExprRenameExt :forall (e : Expr) (ξ1 ξ2 : nat -> nat),
(forall n, ξ1 n = ξ2 n) -> e e| ξ1 = e e| ξ2.
Proof using.
intros e ξ1 ξ2 H.
repeat rewrite ExprRenameSpec. apply ExprSubstExt.
intro n; rewrite H; auto.
Qed.
(*
We define identity substitution and renamings.
We require that the substitution behave as an
identity. From that, we can show that the renaming
also behaves as an identity.
*)
Definition ExprIdSubst : nat -> Expr := fun n => ExprVar n.
Parameter ExprIdentitySubstSpec : forall (e : Expr), e [e| ExprIdSubst] = e.
Definition ExprIdRenaming : nat -> nat := fun n => n.
Lemma ExprIdRenamingSpec : forall (e : Expr), e e| ExprIdRenaming = e.
Proof using.
intros e; rewrite ExprRenameSpec; unfold ExprIdRenaming; cbn.
apply ExprIdentitySubstSpec.
Qed.
(*
Substitution with de Bruijn indices usually relies
on `up` constructions on substitutions. These
are used when going past a constructor to ensure
that counting is done correctly.
Since we don't define substitution explicitly
here, nor do we have binders, these aren't used here.
However, we define them for convenience's sake.
We also prove that they do not affect the
identity substitution and renaming.
*)
Definition ExprUpSubst : (nat -> Expr) -> nat -> Expr :=
fun σ n =>
match n with
......@@ -55,15 +138,7 @@ Module Type Expression.
| S n => S (ξ n)
end.
Parameter ExprSubstExt : forall (e : Expr) (σ1 σ2 : nat -> Expr),
(forall n, σ1 n = σ2 n) -> e [e| σ1] = e [e| σ2].
Parameter ExprRenameExt :forall (e : Expr) (ξ1 ξ2 : nat -> nat),
(forall n, ξ1 n = ξ2 n) -> e e| ξ1 = e e| ξ2.
Definition ExprIdSubst : nat -> Expr := fun n => ExprVar n.
Parameter ExprIdentitySubstSpec : forall (e : Expr), e [e| ExprIdSubst] = e.
Definition ExprIdRenaming : nat -> nat := fun n => n.
Parameter ExprIdRenamingSpec : forall (e : Expr), e e| ExprIdRenaming = e.
Lemma ExprUpSubstId : forall n, ExprIdSubst n = (ExprUpSubst ExprIdSubst) n.
Proof.
intros n; unfold ExprUpSubst; destruct n.
......@@ -75,44 +150,51 @@ Module Type Expression.
intros n; unfold ExprUpRename; destruct n; unfold ExprIdRenaming; reflexivity.
Qed.
Parameter ExprClosedBelowSubst : forall (e : Expr) (σ : nat -> Expr) (n : nat),
ExprClosedBelow n e -> (forall m, m < n -> σ m = ExprVar m) -> e [e|σ] = e.
Parameter ExprClosedAboveSubst : forall (e : Expr) (σ : nat -> Expr) (n : nat),
ExprClosedAbove n e -> (forall m, m < n -> σ m = ExprVar m) -> e [e|σ] = e.
Lemma ExprClosedSubst : forall (e : Expr) (σ : nat -> Expr), ExprClosed e -> e [e|σ] = e.
Proof using.
intros e σ closed; unfold ExprClosed in closed; apply ExprClosedBelowSubst with (n := 0);
intros e σ closed; unfold ExprClosed in closed; apply ExprClosedAboveSubst with (n := 0);
auto.
intros m lt; inversion lt.
Qed.
(*
We require separate boolean expressions `true` and `false`.
These must be separate expressions, and both be values.
*)
Parameter tt ff : Expr.
Parameter ttValue : ExprVal tt.
Parameter ffValue : ExprVal ff.
Parameter boolSeperation : tt <> ff.
(*
ExprStep is the small-step semantics for the
local language. We require that values not be
able to take a step, which reflects the fact that
we are using _small_-step semantics.
*)
Parameter ExprStep : Expr -> Expr -> Prop.
Parameter NoExprStepFromVal : forall v, ExprVal v -> forall e, ~ ExprStep v e.
Parameter ExprRenameClosedBelow : forall e n ξ m,
(*
Substitution, renaming, and stepping
should not change the fact that
expressions are closed above some level.
*)
Parameter ExprRenameClosedAbove : forall e n ξ m,
(forall k, k < n -> ξ k < m) ->
ExprClosedBelow n e ->
ExprClosedBelow m (e e| ξ⟩).
Parameter ExprSubstClosedBelow : forall e n σ m,
(forall k, k < n -> ExprClosedBelow m (σ k)) ->
ExprClosedBelow n e ->
ExprClosedBelow m (e [e| σ]).
ExprClosedAbove n e ->
ExprClosedAbove m (e e| ξ⟩).
Parameter ExprSubstClosedAbove : forall e n σ m,
(forall k, k < n -> ExprClosedAbove m (σ k)) ->
ExprClosedAbove n e ->
ExprClosedAbove m (e [e| σ]).
Parameter ExprClosedAfterStep : forall e1 e2 n,
ExprStep e1 e2 -> ExprClosedBelow n e1 -> ExprClosedBelow n e2.
(* Parameter ExprOpenVal : Expr -> Prop. *)
(* Parameter OpenValRename : *)
(* forall e ξ, ExprOpenVal e -> ExprOpenVal (e e|ξ⟩). *)
(* Parameter OpenValSubst : *)
(* forall e σ, ExprOpenVal e -> (forall n, ExprOpenVal (σ n)) -> ExprOpenVal (e [e|σ]). *)
(* Parameter OpenValFromSubst : forall e σ, ExprOpenVal (e [e| σ]) -> ExprOpenVal e. *)
(* Parameter ValToOpenVal : forall e, ExprVal e -> ExprOpenVal e. *)
(* Parameter VarToOpenVal : forall n, ExprOpenVal (ExprVar n). *)
(* Parameter NoStepFromOpenVal : forall e1, ExprOpenVal e1 -> forall e2, ~ ExprStep e1 e2. *)
(* Parameter IsOpenVal : Expr -> bool. *)
(* Parameter IsOpenValSpec : forall e, IsOpenVal e = true <-> ExprOpenVal e. *)
End Expression.
ExprStep e1 e2 -> ExprClosedAbove n e1 -> ExprClosedAbove n e2.
End LocalLang.
......@@ -8,266 +8,15 @@ Require Import Coq.Sorting.Mergesort.
(*
A module describing the properties of locations in
choreographies and our process calculus. Locations are
ordered (with equality the usual leibniz equality.
This is inspired by FullUsualOrderedType. However,
we're using a set, not a type. Thus, it's a separate
module type, and I give a functor to translate to a
FullUsualOrderedType. This functor is useful for FMaps.
(However, I might build my own FMap later using BSTs,
because that's much better than ordered lists.)
Pirouette. Locations are simply any Set with a
decidable equality relation.
*)
Module Type Locations.
Parameter Inline(10) t : Set.
(* Parameter Inline(40) lt : t -> t -> Prop. *)
(* Parameter Inline(40) le : t -> t -> Prop. *)
(* Axiom le_lteq : forall x y : t, le x y <-> lt x y \/ x = y. *)
Declare Instance eq_equiv : @Equivalence t eq.
Parameter eq_dec : forall x y : t, {x = y} + {x <> y}.
(* Parameter Nontrivial : t. *) (* We don't want to talk about a trivial theory *)
(* Declare Instance lt_strorder : StrictOrder lt. *)
(* Declare Instance lt_compat : Proper (eq ==> eq ==> iff) lt. *)
(* Parameter Inline compare : t -> t -> comparison. *)
(* Axiom cmp_spec : forall x y : t, CompareSpec (x = y) (lt x y) (lt y x) (compare x y). *)
End Locations.
(* Module LocationNotations (L : Locations). *)
(* Infix "<" := L.lt. *)
(* Notation "x > y" := (y < x) (only parsing). *)
(* Notation "x < y < z" := (x < y /\ y < z) (only parsing). *)
(* Infix "<=" := L.le. *)
(* Notation "x >= y" := (y <= x) (only parsing). *)
(* Notation "x <= y <= z" := (x <= y /\ y <= z) (only parsing). *)
(* Infix "?=" := L.compare (at level 70, no associativity). *)
(* End LocationNotations. *)
(* Module LocationFacts (L : Locations). *)
(* Include (LocationNotations L). *)
(* Instance le_refl : Reflexive L.le. *)
(* unfold Reflexive. intro x. apply <- L.le_lteq. right; reflexivity. *)
(* Defined. *)
(* Instance le_trans : Transitive L.le. *)
(* unfold Transitive. intros x y z x_le_y y_le_z. *)
(* rewrite L.le_lteq in x_le_y. rewrite L.le_lteq in y_le_z. *)
(* rewrite L.le_lteq. *)
(* destruct x_le_y as [x_lt_y | eq]; subst; auto. *)
(* destruct y_le_z as [y_lt_z | eq]; subst; auto. *)
(* left; transitivity y; auto. *)
(* Defined. *)
(* Theorem lt_irrefl : forall x : L.t, ~ x < x. *)
(* Proof using. *)
(* intro x. assert (complement L.lt x x) as H. reflexivity. unfold complement in H; exact H. *)
(* Qed. *)
(* Theorem lt_to_le : forall x y : L.t, x < y -> x <= y. *)
(* Proof using. *)
(* intros x y H; rewrite L.le_lteq; left; exact H. *)
(* Qed. *)
(* Theorem compare_Eq_to_eq : forall (x y : L.t), x ?= y = Eq -> x = y. *)
(* Proof using. *)
(* intros x y H. remember (L.cmp_spec x y) as c; inversion c; auto. *)
(* assert (Lt = Eq) as r by (transitivity (x ?= y); auto); discriminate r. *)
(* assert (Gt = Eq) as r by (transitivity (x ?= y); auto); discriminate r. *)
(* Qed. *)
(* Theorem compare_Lt_to_lt : forall (x y : L.t), x ?= y = Lt -> x < y. *)
(* Proof using. *)
(* intros x y H. remember (L.cmp_spec x y) as c; inversion c; auto. *)
(* assert (Eq = Lt) as r by (transitivity (x ?= y); auto); discriminate r. *)
(* assert (Gt = Lt) as r by (transitivity (x ?= y); auto); discriminate r. *)
(* Qed. *)
(* Theorem compare_Gt_to_gt : forall (x y : L.t), x ?= y = Gt -> x > y. *)
(* Proof using. *)
(* intros x y H. remember (L.cmp_spec x y) as c; inversion c; auto. *)
(* assert (Eq = Gt) as r by (transitivity (x ?= y); auto); discriminate r. *)
(* assert (Lt = Gt) as r by (transitivity (x ?= y); auto); discriminate r. *)
(* Qed. *)
(* Ltac LocationOrder := *)
(* repeat match goal with *)
(* | [ H : ?l < ?l |- _ ] => exfalso; apply (lt_irrefl l); exact H *)
(* | [ H : ?l <> ?l |- _ ] => exfalso; apply H; reflexivity; auto *)
(* | [ H : Some _ = None |- _ ] => inversion H *)
(* | [ H1 : ?l1 < ?l2, H2 : ?l2 < ?l1 |- _ ] => exfalso; apply (lt_irrefl l1); transitivity l2; [exact H1 | exact H2] *)
(* | [ H1 : ?l1 < ?l2, H2 : ?l2 < ?l3, H3 : ?l3 < ?l1 |- _ ] => exfalso; apply (lt_irrefl l1); transitivity l2; [exact H1 | transitivity l3; [exact H2 | exact H3]] *)
(* | [ H1 : ?l1 < ?l2, H2 : ?l2 <= ?l1 |- _ ] => apply L.le_lteq in H2; destruct H2; subst *)
(* | [ |- ?l <= ?l ] => reflexivity *)
(* | [ H : ?l1 < ?l2 |- ?l1 <= ?l2 ] => apply lt_to_le; exact H *)
(* | [ H1 : ?l1 <= ?l2, H2 : ?l2 <= ?l3 |- ?l1 <= ?l3 ] => transitivity l2; [exact H1 | exact H2] *)
(* | [ H1 : ?l1 < ?l2, H2 : ?l2 < ?l3 |- ?l1 <= ?l3 ] => apply lt_to_le; transitivity l2; [exact H1 | exact H2] *)
(* | [ H1 : ?l1 < ?l2, H2 : ?l2 <= ?l3 |- ?l1 <= ?l3 ] => transitivity l2; [apply lt_to_le; exact H1 | exact H2] *)
(* | [ H : Some ?l1 = Some ?l2 |- _] => inversion H; subst; clear H *)
(* | [ H : (?l ?= ?l') = Eq |- _ ] => apply compare_Eq_to_eq in H; subst *)
(* | [ H : (?l ?= ?l') = Lt |- _ ] => apply compare_Lt_to_lt in H *)
(* | [ H : (?l ?= ?l') = Gt |- _ ] => apply compare_Gt_to_gt in H *)
(* | [ H : Eq = (?l ?= ?l') |- _ ] => symmetry in H; apply compare_Eq_to_eq in H; subst *)
(* | [ H : Lt = (?l ?= ?l') |- _ ] => symmetry in H; apply compare_Lt_to_lt in H *)
(* | [ H : Gt = (?l ?= ?l') |- _ ] => symmetry in H; apply compare_Gt_to_gt in H *)
(* end; auto. *)
(* Ltac DestructCompare x y := *)
(* let x_y := fresh x "_" y in *)
(* destruct (x ?= y) eqn:x_y; cbn in *; LocationOrder. *)
(* Definition le_bool : L.t -> L.t -> bool := *)
(* fun l1 l2 => match L.compare l1 l2 with *)
(* | Gt => false *)
(* | _ => true *)
(* end. *)
(* Notation "l1 <=? l2" := (le_bool l1 l2) (at level 70). *)