From 0d7365e6ddcbd14933fcedae777649d31fb311cc Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 15 Mar 2019 17:33:58 +0100 Subject: EConstr iterators respect the binding structure of cases. Fixes #3166. --- test-suite/bugs/closed/bug_3166.v | 84 +++++++++++++++++++++++++++++++++++++++ test-suite/bugs/opened/bug_3166.v | 84 --------------------------------------- 2 files changed, 84 insertions(+), 84 deletions(-) create mode 100644 test-suite/bugs/closed/bug_3166.v delete mode 100644 test-suite/bugs/opened/bug_3166.v (limited to 'test-suite') diff --git a/test-suite/bugs/closed/bug_3166.v b/test-suite/bugs/closed/bug_3166.v new file mode 100644 index 0000000000..3b3375fdd8 --- /dev/null +++ b/test-suite/bugs/closed/bug_3166.v @@ -0,0 +1,84 @@ +Set Asymmetric Patterns. + +Section eq. + Let A := { X : Type & X }. + Let B := (fun x : A => projT1 x). + Let T := (fun (a' : A) (b' : B a') => projT2 a' = b'). + Let T' := T. + Let t1T := (fun _ : A => unit). + Let f1 := (fun x (_ : t1T x) => projT2 x). + Let t1 := (fun x (y : t1T x) => @eq_refl (projT1 x) (projT2 x)). + Let t1T' := t1T. + Let f1' := f1. + Let t1' := t1. + + Theorem eq_matches_commute + a' b' (t' : T a' b') + (rta : forall b'', T' a' b'' -> A) + (rtb : forall b'' t'', B (rta b'' t'')) + (rt1 : forall y, T _ (rtb (f1' a' y) (@t1' a' y))) + (R : forall (b : B (rta b' t')), T _ b -> Type) + (r1 : forall y, R (f1 _ y) (@t1 _ y)) + : match + match t' as t0' in (@eq _ _ b0') return T (rta b0' t0') (rtb b0' t0') with + | eq_refl => rt1 tt + end + as t0 in (@eq _ _ b0) + return R b0 t0 + with + | eq_refl => r1 tt + end + = + match t' + as t0' in (@eq _ _ b0') + return (forall (R : forall (b : B (rta b0' t0')), T _ b -> Type) + (r1 : forall y, R (f1 _ y) (@t1 _ y)), + R _ (match t0' as t0'0 in (@eq _ _ b0'0) return T (rta b0'0 t0'0) (rtb b0'0 t0'0) with + | eq_refl => rt1 tt + end)) + with + | eq_refl => fun _ r1 => + match rt1 tt with + | eq_refl => r1 tt + end + end R r1. + Proof. + destruct t'; reflexivity. + Defined. + + Theorem eq_match_beta2 + a b (t : T a b) + X + (R : forall b' (t' : T a b'), X b' -> Type) + (r1 : forall y x, R _ (@t1 _ y) x) + x + : match t as t' in (@eq _ _ b') return forall x, R b' t' x with + | eq_refl => r1 tt + end (x b) + = + match t as t' in (@eq _ _ b') return R b' t' (x b') with + | eq_refl => r1 tt (x _) + end. + Proof. + destruct t; reflexivity. + Defined. +End eq. + +Definition typeof {T} (_ : T) := T. + +Eval compute in (eq_sym (eq_sym _)). +Goal forall T (x y : T) (p : x = y), True. + intros. + pose proof + (@eq_matches_commute + (existT (fun T => T) T x) y p + (fun b'' _ => existT (fun T => T) T b'') + (fun _ _ => x) + (fun _ => eq_refl) + (fun x' _ => x' = y) + (fun _ => eq_refl) + ) as H0. + compute in H0. + change (fun (x' : T) (_ : y = x') => x' = y) with ((fun y => fun (x' : T) (_ : y = x') => x' = y) y) in H0. + pose proof (fun k => @eq_trans _ _ _ k H0). +Abort. diff --git a/test-suite/bugs/opened/bug_3166.v b/test-suite/bugs/opened/bug_3166.v deleted file mode 100644 index baf87631f0..0000000000 --- a/test-suite/bugs/opened/bug_3166.v +++ /dev/null @@ -1,84 +0,0 @@ -Set Asymmetric Patterns. - -Section eq. - Let A := { X : Type & X }. - Let B := (fun x : A => projT1 x). - Let T := (fun (a' : A) (b' : B a') => projT2 a' = b'). - Let T' := T. - Let t1T := (fun _ : A => unit). - Let f1 := (fun x (_ : t1T x) => projT2 x). - Let t1 := (fun x (y : t1T x) => @eq_refl (projT1 x) (projT2 x)). - Let t1T' := t1T. - Let f1' := f1. - Let t1' := t1. - - Theorem eq_matches_commute - a' b' (t' : T a' b') - (rta : forall b'', T' a' b'' -> A) - (rtb : forall b'' t'', B (rta b'' t'')) - (rt1 : forall y, T _ (rtb (f1' a' y) (@t1' a' y))) - (R : forall (b : B (rta b' t')), T _ b -> Type) - (r1 : forall y, R (f1 _ y) (@t1 _ y)) - : match - match t' as t0' in (@eq _ _ b0') return T (rta b0' t0') (rtb b0' t0') with - | eq_refl => rt1 tt - end - as t0 in (@eq _ _ b0) - return R b0 t0 - with - | eq_refl => r1 tt - end - = - match t' - as t0' in (@eq _ _ b0') - return (forall (R : forall (b : B (rta b0' t0')), T _ b -> Type) - (r1 : forall y, R (f1 _ y) (@t1 _ y)), - R _ (match t0' as t0'0 in (@eq _ _ b0'0) return T (rta b0'0 t0'0) (rtb b0'0 t0'0) with - | eq_refl => rt1 tt - end)) - with - | eq_refl => fun _ r1 => - match rt1 tt with - | eq_refl => r1 tt - end - end R r1. - Proof. - destruct t'; reflexivity. - Defined. - - Theorem eq_match_beta2 - a b (t : T a b) - X - (R : forall b' (t' : T a b'), X b' -> Type) - (r1 : forall y x, R _ (@t1 _ y) x) - x - : match t as t' in (@eq _ _ b') return forall x, R b' t' x with - | eq_refl => r1 tt - end (x b) - = - match t as t' in (@eq _ _ b') return R b' t' (x b') with - | eq_refl => r1 tt (x _) - end. - Proof. - destruct t; reflexivity. - Defined. -End eq. - -Definition typeof {T} (_ : T) := T. - -Eval compute in (eq_sym (eq_sym _)). -Goal forall T (x y : T) (p : x = y), True. - intros. - pose proof - (@eq_matches_commute - (existT (fun T => T) T x) y p - (fun b'' _ => existT (fun T => T) T b'') - (fun _ _ => x) - (fun _ => eq_refl) - (fun x' _ => x' = y) - (fun _ => eq_refl) - ) as H0. - compute in H0. - change (fun (x' : T) (_ : y = x') => x' = y) with ((fun y => fun (x' : T) (_ : y = x') => x' = y) y) in H0. - Fail pose proof (fun k => @eq_trans _ _ _ k H0). -Abort. -- cgit v1.2.3 From fd50f21cfe2460fa35fe962390f4ba810d7ca837 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 15 Mar 2019 18:39:48 +0100 Subject: Temporarily deactivating printing check for cases. Destruct has changed semantics, but I'd like to see how CI fares so far. --- test-suite/output/Cases.out | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) (limited to 'test-suite') diff --git a/test-suite/output/Cases.out b/test-suite/output/Cases.out index 984ac4e527..6fd4d37ab4 100644 --- a/test-suite/output/Cases.out +++ b/test-suite/output/Cases.out @@ -50,10 +50,11 @@ f = fun H : B => match H with | AC x => - let b0 := b in - (if b0 as b return (P b -> True) - then fun _ : P true => Logic.I - else fun _ : P false => Logic.I) x + (fun x0 : P b => + let b0 := b in + (if b0 as b return (P b -> True) + then fun _ : P true => Logic.I + else fun _ : P false => Logic.I) x0) x end : B -> True The command has indeed failed with message: -- cgit v1.2.3