diff options
author | Samuel Mimram <smimram@debian.org> | 2006-04-28 14:59:16 +0000 |
---|---|---|
committer | Samuel Mimram <smimram@debian.org> | 2006-04-28 14:59:16 +0000 |
commit | 3ef7797ef6fc605dfafb32523261fe1b023aeecb (patch) | |
tree | ad89c6bb57ceee608fcba2bb3435b74e0f57919e /test-suite/success/refine.v | |
parent | 018ee3b0c2be79eb81b1f65c3f3fa142d24129c8 (diff) |
Imported Upstream version 8.0pl3+8.1alphaupstream/8.0pl3+8.1alpha
Diffstat (limited to 'test-suite/success/refine.v')
-rw-r--r-- | test-suite/success/refine.v | 68 |
1 files changed, 52 insertions, 16 deletions
diff --git a/test-suite/success/refine.v b/test-suite/success/refine.v index ad4eed5a..b61cf275 100644 --- a/test-suite/success/refine.v +++ b/test-suite/success/refine.v @@ -1,30 +1,66 @@ (* Refine and let-in's *) -Goal (EX x:nat | x=O). -Refine let y = (plus O O) in ?. -Exists y; Auto. +Goal exists x : nat, x = 0. + refine (let y := 0 + 0 in _). +exists y; auto. Save test1. -Goal (EX x:nat | x=O). -Refine let y = (plus O O) in (ex_intro ? ? (plus y y) ?). -Auto. +Goal exists x : nat, x = 0. + refine (let y := 0 + 0 in ex_intro _ (y + y) _). +auto. Save test2. Goal nat. -Refine let y = O in (plus O ?). -Exact (S O). + refine (let y := 0 in 0 + _). +exact 1. Save test3. (* Example submitted by Yves on coqdev *) -Require PolyList. +Require Import List. -Goal (l:(list nat))l=l. +Goal forall l : list nat, l = l. Proof. -Refine [l]<[l]l=l> - Cases l of - | nil => ? - | (cons O l0) => ? - | (cons (S _) l0) => ? - end. + refine + (fun l => + match l return (l = l) with + | nil => _ + | O :: l0 => _ + | S _ :: l0 => _ + end). +Abort. + +(* Submitted by Roland Zumkeller (bug #888) *) + +(* The Fix and CoFix rules expect a subgoal even for closed components of the + (co-)fixpoint *) + +Goal nat -> nat. + refine (fix f (n : nat) : nat := S _ + with pred (n : nat) : nat := n + for f). +exact 0. +Qed. + +(* Submitted by Roland Zumkeller (bug #889) *) + +(* The types of metas were in metamap and they were not updated when + passing through a binder *) + +Goal forall n : nat, nat -> n = 0. + refine + (fun n => fix f (i : nat) : n = 0 := match i with + | O => _ + | S _ => _ + end). +Abort. + +(* Submitted by Roland Zumkeller (bug #931) *) +(* Don't turn dependent evar into metas *) + +Goal (forall n : nat, n = 0 -> Prop) -> Prop. +intro P. + refine (P _ _). +reflexivity. +Abort. |