edf804c70f
This PR generalizes the `noConfusion` constructions to heterogeneous equalities (assuming propositional equalities between the indices). This lays ground work for better support for applying injection to heterogeneous equalities in grind. The `Meta.mkNoConfusion` app builder shields most of the code from these changes. Since the per-constructor noConfusion principles are now more expressive, `Meta.mkNoConfusion` no longer uses the general one. In `Init.Prelude` some proofs are more pedestrian because `injection` now needs a bit more machinery. This is a breaking change for whoever uses the `noConfusion` principle manually and explicitly for a type with indices. Fixes #11450.
29 lines
767 B
Text
29 lines
767 B
Text
opaque double : Nat → Nat
|
|
|
|
inductive Parity : Nat -> Type
|
|
| even (n) : Parity (double n)
|
|
| odd (n) : Parity (Nat.succ (double n))
|
|
|
|
example
|
|
(motive : (x : Nat) → Parity x → Sort u_1)
|
|
(h_2 : (j : Nat) → motive (double j) (Parity.even j))
|
|
(j n : Nat)
|
|
(heq_1 : double n = double j)
|
|
(heq_2 : Parity.even n ≍ Parity.even j):
|
|
h_2 n ≍ h_2 j := by
|
|
fail_if_success grind -- does not work yet
|
|
sorry
|
|
|
|
-- manual proof using heterogenenous noConfusion
|
|
|
|
example
|
|
(motive : (x : Nat) → Parity x → Sort u_1)
|
|
(h_2 : (j : Nat) → motive (double j) (Parity.even j))
|
|
(j n : Nat)
|
|
(heq_1 : double n = double j)
|
|
(heq_2 : Parity.even n ≍ Parity.even j):
|
|
h_2 n ≍ h_2 j := by
|
|
apply Parity.noConfusion heq_1 heq_2
|
|
intro hnj
|
|
subst hnj
|
|
rfl
|