summaryrefslogtreecommitdiff
path: root/test-suite/success/fix.v
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <smimram@debian.org>2006-04-28 14:59:16 +0000
committerGravatar Samuel Mimram <smimram@debian.org>2006-04-28 14:59:16 +0000
commit3ef7797ef6fc605dfafb32523261fe1b023aeecb (patch)
treead89c6bb57ceee608fcba2bb3435b74e0f57919e /test-suite/success/fix.v
parent018ee3b0c2be79eb81b1f65c3f3fa142d24129c8 (diff)
Imported Upstream version 8.0pl3+8.1alphaupstream/8.0pl3+8.1alpha
Diffstat (limited to 'test-suite/success/fix.v')
-rw-r--r--test-suite/success/fix.v63
1 files changed, 32 insertions, 31 deletions
diff --git a/test-suite/success/fix.v b/test-suite/success/fix.v
index 374029bb..f4a4d36d 100644
--- a/test-suite/success/fix.v
+++ b/test-suite/success/fix.v
@@ -12,40 +12,41 @@ Require Import ZArith.
Definition rNat := positive.
-Inductive rBoolOp: Set :=
- rAnd: rBoolOp
- | rEq: rBoolOp .
-
-Definition rlt: rNat -> rNat ->Prop := [a, b:rNat](compare a b EGAL)=INFERIEUR.
-
-Definition rltDec: (m, n:rNat){(rlt m n)}+{(rlt n m) \/ m=n}.
-Intros n m; Generalize (compare_convert_INFERIEUR n m);
- Generalize (compare_convert_SUPERIEUR n m);
- Generalize (compare_convert_EGAL n m); Case (compare n m EGAL).
-Intros H' H'0 H'1; Right; Right; Auto.
-Intros H' H'0 H'1; Left; Unfold rlt.
-Apply convert_compare_INFERIEUR; Auto.
-Intros H' H'0 H'1; Right; Left; Unfold rlt.
-Apply convert_compare_INFERIEUR; Auto.
-Apply H'0; Auto.
+Inductive rBoolOp : Set :=
+ | rAnd : rBoolOp
+ | rEq : rBoolOp.
+
+Definition rlt (a b : rNat) : Prop :=
+ (a ?= b)%positive Datatypes.Eq = Datatypes.Lt.
+
+Definition rltDec : forall m n : rNat, {rlt m n} + {rlt n m \/ m = n}.
+intros n m; generalize (nat_of_P_lt_Lt_compare_morphism n m);
+ generalize (nat_of_P_gt_Gt_compare_morphism n m);
+ generalize (Pcompare_Eq_eq n m); case ((n ?= m)%positive Datatypes.Eq).
+intros H' H'0 H'1; right; right; auto.
+intros H' H'0 H'1; left; unfold rlt in |- *.
+apply nat_of_P_lt_Lt_compare_complement_morphism; auto.
+intros H' H'0 H'1; right; left; unfold rlt in |- *.
+apply nat_of_P_lt_Lt_compare_complement_morphism; auto.
+apply H'0; auto.
Defined.
-Definition rmax: rNat -> rNat ->rNat.
-Intros n m; Case (rltDec n m); Intros Rlt0.
-Exact m.
-Exact n.
+Definition rmax : rNat -> rNat -> rNat.
+intros n m; case (rltDec n m); intros Rlt0.
+exact m.
+exact n.
Defined.
-Inductive rExpr: Set :=
- rV: rNat ->rExpr
- | rN: rExpr ->rExpr
- | rNode: rBoolOp -> rExpr -> rExpr ->rExpr .
-
-Fixpoint maxVar[e:rExpr]: rNat :=
- Cases e of
- (rV n) => n
- | (rN p) => (maxVar p)
- | (rNode n p q) => (rmax (maxVar p) (maxVar q))
- end.
+Inductive rExpr : Set :=
+ | rV : rNat -> rExpr
+ | rN : rExpr -> rExpr
+ | rNode : rBoolOp -> rExpr -> rExpr -> rExpr.
+
+Fixpoint maxVar (e : rExpr) : rNat :=
+ match e with
+ | rV n => n
+ | rN p => maxVar p
+ | rNode n p q => rmax (maxVar p) (maxVar q)
+ end.