diff options
Diffstat (limited to 'test-suite/bugs/closed/2456.v')
| -rw-r--r-- | test-suite/bugs/closed/2456.v | 58 |
1 files changed, 58 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/2456.v b/test-suite/bugs/closed/2456.v new file mode 100644 index 00000000..de28c7f4 --- /dev/null +++ b/test-suite/bugs/closed/2456.v @@ -0,0 +1,58 @@ + +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. +revert X. +dependent destruction commute1; +dependent destruction catchCommuteDetails; +dependent destruction commute2; +dependent destruction catchCommuteDetails. +Abort. |