summaryrefslogtreecommitdiff
path: root/test-suite/bugs/closed/shouldsucceed/2456.v
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2012-01-12 16:02:20 +0100
committerGravatar Stephane Glondu <steph@glondu.net>2012-01-12 16:02:20 +0100
commit97fefe1fcca363a1317e066e7f4b99b9c1e9987b (patch)
tree97ec6b7d831cc5fb66328b0c63a11db1cbb2f158 /test-suite/bugs/closed/shouldsucceed/2456.v
parent300293c119981054c95182a90c829058530a6b6f (diff)
Imported Upstream version 8.4~betaupstream/8.4_beta
Diffstat (limited to 'test-suite/bugs/closed/shouldsucceed/2456.v')
-rw-r--r--test-suite/bugs/closed/shouldsucceed/2456.v53
1 files changed, 53 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/shouldsucceed/2456.v b/test-suite/bugs/closed/shouldsucceed/2456.v
new file mode 100644
index 00000000..56f046c4
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2456.v
@@ -0,0 +1,53 @@
+
+Require Import Equality.
+
+Parameter Patch : nat -> nat -> Set.
+
+Inductive Catch (from to : nat) : Type
+ := MkCatch : forall (p : Patch from to),
+ Catch from to.
+Implicit Arguments MkCatch [from to].
+
+Inductive CatchCommute5
+ : forall {from mid1 mid2 to : nat},
+ Catch from mid1
+ -> Catch mid1 to
+ -> Catch from mid2
+ -> Catch mid2 to
+ -> Prop
+ := MkCatchCommute5 :
+ forall {from mid1 mid2 to : nat}
+ (p : Patch from mid1)
+ (q : Patch mid1 to)
+ (q' : Patch from mid2)
+ (p' : Patch mid2 to),
+ CatchCommute5 (MkCatch p) (MkCatch q) (MkCatch q') (MkCatch p').
+
+Inductive CatchCommute {from mid1 mid2 to : nat}
+ (p : Catch from mid1)
+ (q : Catch mid1 to)
+ (q' : Catch from mid2)
+ (p' : Catch mid2 to)
+ : Prop
+ := isCatchCommute5 : forall (catchCommuteDetails : CatchCommute5 p q q' p'),
+ CatchCommute p q q' p'.
+Notation "<< p , q >> <~> << q' , p' >>"
+ := (CatchCommute p q q' p')
+ (at level 60, no associativity).
+
+Lemma CatchCommuteUnique2 :
+ forall {from mid mid' to : nat}
+ {p : Catch from mid} {q : Catch mid to}
+ {q' : Catch from mid'} {p' : Catch mid' to}
+ {q'' : Catch from mid'} {p'' : Catch mid' to}
+ (commute1 : <<p, q>> <~> <<q', p'>>)
+ (commute2 : <<p, q>> <~> <<q'', p''>>),
+ (p' = p'') /\ (q' = q'').
+Proof with auto.
+intros.
+set (X := commute2).
+dependent destruction commute1;
+dependent destruction catchCommuteDetails;
+dependent destruction commute2;
+dependent destruction catchCommuteDetails generalizing X.
+Admitted. \ No newline at end of file