max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix: make sure noConfusionTypeEnum and noConfusionEnum fully reduce even reducibility setting is set to TransparencyMode.reducible

Browse source 
The previous definition would not fully reduce since `ite` and `dite`
are not tagged as `[reducible]`.

see issue #1016
This commit is contained in:
Leonardo de Moura 2022-02-14 11:37:23 -08:00
parent bdbffdaaf7
commit 420d0f2a3f
1 changed files with 10 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

17
src/Init/Core.lean
View file

@ -446,14 +446,17 @@ instance {c : Prop} {t : c → Prop} {e : ¬c → Prop} [dC : Decidable c] [dT :
| isFalse hc => dE hc
/- Auxiliary definitions for generating compact `noConfusion` for enumeration types -/
abbrev noConfusionTypeEnum {α : Sort u} {β : Sort v} [DecidableEq β] (f : α → β) (P : Sort w) (x y : α) : Sort w :=
if f x = f y then P → P else P
abbrev noConfusionTypeEnum {α : Sort u} {β : Sort v} [inst : DecidableEq β] (f : α → β) (P : Sort w) (x y : α) : Sort w :=
Decidable.casesOn (motive := fun _ => Sort w) (inst (f x) (f y))
(fun _ => P)
(fun _ => P → P)
abbrev noConfusionEnum {α : Sort u} {β : Sort v} [DecidableEq β] (f : α → β) {P : Sort w} {x y : α} (h : x = y) : noConfusionTypeEnum f P x y :=
if h' : f x = f y then
cast (@if_pos _ _ h' _ (P → P) (P)).symm (fun (h : P) => h)
else
False.elim (h' (congrArg f h))
abbrev noConfusionEnum {α : Sort u} {β : Sort v} [inst : DecidableEq β] (f : α → β) {P : Sort w} {x y : α} (h : x = y) : noConfusionTypeEnum f P x y :=
Decidable.casesOn
(motive := fun (inst : Decidable (f x = f y)) => Decidable.casesOn (motive := fun _ => Sort w) inst (fun _ => P) (fun _ => P → P))
(inst (f x) (f y))
(fun h' => False.elim (h' (congrArg f h)))
(fun h' => fun x => x)
/- Inhabited -/