diff options
Diffstat (limited to 'test-suite/bugs/opened/2456.v')
-rw-r--r-- | test-suite/bugs/opened/2456.v | 53 |
1 files changed, 0 insertions, 53 deletions
diff --git a/test-suite/bugs/opened/2456.v b/test-suite/bugs/opened/2456.v deleted file mode 100644 index 6cca5c9f..00000000 --- a/test-suite/bugs/opened/2456.v +++ /dev/null @@ -1,53 +0,0 @@ - -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). -Fail dependent destruction commute1; -dependent destruction catchCommuteDetails; -dependent destruction commute2; -dependent destruction catchCommuteDetails generalizing X. -Admitted. |