Commit 83db6873 authored by Andrew Hirsch's avatar Andrew Hirsch
Browse files

Removing more extraneous assumptions.

parent df573b11
......@@ -10,18 +10,18 @@ Module Type Expression.
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.
(* 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. *)
Parameter ExprSubst : Expr -> (nat -> Expr) -> Expr.
Parameter ExprRename : Expr -> (nat -> nat) -> Expr.
......
......@@ -29,7 +29,7 @@ Module Type Locations.
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 *)
(* 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. *)
......
Supports Markdown
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