Dependent pattern match compilation – other languages?

Stream: lean4

[Joachim Breitner]

I am currently fighting with Lean to properly support a dependent pattern match like

inductive Parity : Nat -> Type
| even (n) : Parity (n + n)
| odd  (n) : Parity (Nat.succ (n + n))

partial def natToBin3 : (n : Nat) → Parity n →  List Bool
| 0, _             => []
| _, Parity.even j => [false, false]
| _, Parity.odd  j => [true, true]

In fact, before 4.26, the whole match would not be accepted; since 4.25 the match works, but Lean (and I) struggle to get the equational theorems derived for that.

How do other dependently typed languages fare with this example? Any Rocq, Agda, Idris users reading this who could quickly type the corresponding code into their system and see if it can handle it?

And does/can your system now prove the equivalent of the equational lemma?

natToBin3.eq_2 (j : Nat) (h : j + j ≠ 0) : natToBin3 (j + j) (Parity.even j) = [false, false]

[Arthur Adjedj]

From the Rocq side of things, defining the functions using match works as expected, although Equations fails:

From Equations Require Import Equations.

Inductive Parity : nat -> Type :=
| even n : Parity (n + n)
| odd  n : Parity (S (n + n)).

(*works*)
Definition natToBin3 (n : nat) (p :Parity n): list bool :=
  match n,p with
    | 0, _             => nil
    | _, even j => cons false (cons false nil)
    | _, odd  j => cons true (cons true nil)
  end.

(*Unable to build a covering for:
natToBin3 n p
In context:
 n : nat
 p : Parity n*)
Fail Equations natToBin3 (n : nat) (p :Parity n): list bool :=
    natToBin3 0 _             := nil;
    natToBin3 _ (even j) := cons false (cons false nil);
    natToBin3 _ (odd  j) := cons true (cons true nil).

As for the theorem, I can't manage to do much with it. This is provably provable, I'm just not sure how.

[Jean Abou Samra]

This works in Rocq:

Require Import Lia List. Import ListNotations.

Inductive Parity : nat -> Type :=
| even n : Parity (n + n)
| odd  n : Parity (S (n + n)).

Definition natToBin3 (n : nat) (p :Parity n): list bool :=
  match n,p with
    | 0, _ => []
    | _, even j => [false; false]
    | _, odd  j => [true; true]
  end.

Lemma natToBin3_eq (j : nat) (h : j + j <> 0) :
  natToBin3 (j + j) (even j) = [false; false].
Proof.
  destruct j.
  - lia.
  - reflexivity.
Qed.

[Jean Abou Samra]

Agda doesn't accept this pattern matching (I'm not sure why):

open import Data.Nat
open import Data.Bool
open import Data.List.Base

data Parity : ℕ → Set where
  even : (n : ℕ) → Parity (n + n)
  odd : (n : ℕ) → Parity (suc (n + n))

nat-to-bin3 : (n : ℕ) → Parity n → List Bool
nat-to-bin3 0 _ = []
nat-to-bin3 .(n + n) (even n) = false ∷ false ∷ []
nat-to-bin3 .(suc (n + n)) (odd n) = true ∷ true ∷ []

[Jean Abou Samra]

It says

I'm not sure if there should be a case for the constructor even,
because I get stuck when trying to solve the following unification
problems (inferred index ≟ expected index):
  n + n ≟ suc n₁
when checking the definition of nat-to-bin3

[Jean Abou Samra]

https://agda.zulipchat.com/#narrow/channel/238741-general/topic/Why.20is.20this.20pattern.20matching.20rejected.3F/with/560807747

[Jean Abou Samra]

Lean (and I) struggle to get the equational theorems derived for that.

For what it's worth, the equational lemma is provable in Lean in exactly the same way as in Rocq:

inductive Parity : Nat -> Type
| even (n) : Parity (n + n)
| odd  (n) : Parity (Nat.succ (n + n))

partial def natToBin3 : (n : Nat) → Parity n →  List Bool
| 0, _             => []
| _, Parity.even j => [false, false]
| _, Parity.odd  j => [true, true]

def natToBin3_eq (j : Nat) (h : j + j ≠ 0) : natToBin3 (j + j) (Parity.even j) = [false, false] := by
  cases j
  . omega
  . rfl

[Joachim Breitner]

Ah, yes, I think I can do it manually; what I struggle with is writing meta-code that does it reliably and reasonably efficiently in general.

In this case, it takes “cleverness” to recognize that cases j means that we can get j + j past the Nat.casesOn. In general, that won’t work.

You can read more on what I tried and where I got stuck in my inner monologue at https://github.com/leanprover/lean4/pull/11342 if you are curious.

[Joachim Breitner]

And it seems that both Rocq Equations and Agda run into comparable problems here.

[Jean Abou Samra]

Joachim Breitner said:

And it seems that both Rocq Equations and Agda run into comparable problems here.

IIUC they're inspired from the same lines of work (by Conor McBride, Jesper Cockx and others) so that's not too surprising.

[Yves Jäckle]

Played around a bit and got no solutions, but more experiments, in case they're of interest:
live-lean

inductive Parity : Nat -> Type
| even (n) : Parity (n + n)
| odd  (n) : Parity (Nat.succ (n + n))

def natToBin3 : (n : Nat) → Parity n →  List Bool
| 0, _             => []
| _, Parity.even j => [false, false]
| _, Parity.odd  j => [true, true]


def natToBin2 : (n : Nat) → Parity n →  List Bool
| 0, _             => []
| _, p =>
  match p with
  | Parity.even j => [false, false]
  | Parity.odd  j => [true, true]


example : natToBin3 = natToBin2 := by
  funext n p
  cases p
  · rename_i n; cases n; rfl ; rfl
  · rename_i n; cases n; rfl ; rfl

def natToBin1 : (n : Nat) → Parity n →  List Bool
  | n, p =>
    match p with
    | .even j =>
        match n with
        | 0 => []
        | _ => [false, false]
    | .odd j =>
        match n with
        | 0 => []
        | _ => [true, true]

example (j : Nat) (h : (j + j) = 0 → False) :
  natToBin1 (j + j) (Parity.even j) = [false,false] := by
    rw [natToBin1.eq_1, natToBin2.match_3.eq_2]
    intro _ ohno _ ; exact h ohno

example : natToBin3 = natToBin1 := by
  funext n p
  cases p
  · rename_i n; cases n; rfl ; rfl
  · rename_i n; cases n; rfl ; rfl


def natToBin0 (n : Nat) : Parity n →  List Bool
  | .even j =>
      match n with
      | 0 => []
      | _ => [false, false]
  | .odd j =>
      match n with
      | 0 => []
      | _ => [true, true]


example (j : Nat) (h : (j + j) = 0 → False) :
  natToBin1 (j + j) (Parity.even j) = [false,false] := by
    rw [natToBin1.eq_1, natToBin2.match_3.eq_2]
    intro _ ohno _ ; exact h ohno

example : natToBin3 = natToBin0 := by
  funext n p
  cases p
  · rename_i n; cases n; rfl ; rfl
  · rename_i n; cases n; rfl ; rfl

Don't know if it helps :sweat_smile:

[Joachim Breitner]

Incidentally, your natToBin2 is pretty much how lean compiles natToBin3 since the latest release, before it wouldn't even be accepted

[Joachim Breitner]

So the here is what I am struggling to reconcile:

1. To do a proof about the body of a matcher that needs to explore the branches, I want the discriminants to be as general as in the original matcher (e.g. n not j + j), else I cannot split.
2. But in order to not split those primitive casesOn that are determined by the current equation, I wnat them to be the concrete constructor.

So due to 1 it seems promising to start with variables for the discriminants and add assumptions that they are equal to the pattern of the case we are interested in. And one might think that’s good enough, we can just keep splitting and then unify the equations we get to eliminate the wrong branches and continue to make progress in the right branch. But that doesn’t work with dependencies, as this example shows (I have changed j + j to an opaque double so that grind does not reason by injectivity):

opaque double : Nat → Nat

inductive Parity : Nat -> Type
| even (n) : Parity (double n)
| odd  (n) : Parity (Nat.succ (double n))

def simple : (n : Nat) → Parity n →  List Bool
| _, Parity.even j => [false, false]
| _, Parity.odd  j => [true, true]

set_option pp.match false

/--
info: private theorem simple.match_1.congr_eq_1.{u_1} : ∀ (motive : (x : Nat) → Parity x → Sort u_1) (x : Nat)
  (x_1 : Parity x) (h_1 : (j : Nat) → motive (double j) (Parity.even j))
  (h_2 : (j : Nat) → motive (double j).succ (Parity.odd j)) (j : Nat),
  x = double j → x_1 ≍ Parity.even j → simple.match_1 motive x x_1 h_1 h_2 ≍ h_1 j
-/
#guard_msgs in
#print sig simple.match_1.congr_eq_1

/--
error: unsolved goals
case even
motive : (x : Nat) → Parity x → Sort u_1
alt1 : (j : Nat) → motive (double j) (Parity.even j)
alt2 : (j : Nat) → motive (double j).succ (Parity.odd j)
j n✝ : Nat
hn : double n✝ = double j
hp : Parity.even n✝ ≍ Parity.even j
⊢ alt1 n✝ ≍ alt1 j
-/
#guard_msgs in
theorem congr_eq_1_by_split : ∀ (motive : (x : Nat) → Parity x → Sort u_1) (x : Nat)
  (x_1 : Parity x) (h_1 : (j : Nat) → motive (double j) (Parity.even j))
  (h_2 : (j : Nat) → motive (double j).succ (Parity.odd j)) (j : Nat),
  x = double j → x_1 ≍ Parity.even j → simple.match_1 motive x x_1 h_1 h_2 ≍ h_1 j := by
  intro motive n p alt1 alt2 j hn hp
  unfold simple.match_1; dsimp
  -- works:
  -- subst hn hp; rfl
  cases p
  · dsimp
    -- unsolvable goal, it seems
  · sorry

It seems that Parity.even n✝ ≍ Parity.even j is not good enough to make progress here.

The only way forward I see would be an algorithm that

• keeps the variables abstract, so that we can split our way past the | 0 pattern in natToBin3
• but recognizes when we are about to do a split on p where p ≍ ctor e is in the context, and then substitutes that instead of splitting
• but after (or before) substituting changes e to a variable so that we can make good progress.

Implementing that is very daunting, and it feels too complicated.

Another direction would be to keep the concrete values and only when we hit a Nat.casesOn (double j)we generalize the double j so that we can case split, but now we get these generalized equations into the context and have to reconcile them with overlap assumptions like (h : j + j ≠ 0)

[Joachim Breitner]

One promising direction was to define the equivalent of fun_cases_unfolding for a matcher: A theorem that splits into all the cases and reduces the matcher along the way. This is defineable:

import Lean

inductive Parity : Nat -> Type
| even (n) : Parity (n + n)
| odd  (n) : Parity (Nat.succ (n + n))

partial def natToBin3 : (n : Nat) → Parity n →  List Bool
| 0, _             => []
| _, Parity.even j => [false, false]
| _, Parity.odd  j => [true, true]

-- #check natToBin3.match_1.eq_1

/--
info: natToBin3.match_1.{u_1} (motive : (x : Nat) → Parity x → Sort u_1) (x✝ : Nat) (x✝¹ : Parity x✝)
  (h_1 : (x : Parity 0) → motive 0 x) (h_2 : (j : Nat) → motive (j + j) (Parity.even j))
  (h_3 : (j : Nat) → motive (j + j).succ (Parity.odd j)) : motive x✝ x✝¹
-/
#guard_msgs in
#check natToBin3.match_1

-- #11402
theorem natToBin3._sparseCasesOn_1.else_eq.{u} {motive : Nat → Sort u} (t : Nat) (zero : motive Nat.zero)
  («else»: t.ctorIdx ≠ 0 → motive t) (h : t.ctorIdx ≠ 0) :
  _sparseCasesOn_1 t zero «else» = «else» h := by
  unfold _sparseCasesOn_1
  cases t <;> dsimp
  contradiction

-- fun_cases for sparseCasesOn.
theorem natToBin3._sparseCasesOn_1.unfold.{u}
  {motive : Nat → Sort u} (t : Nat)
  (zero : motive Nat.zero) («else»: t.ctorIdx ≠ 0 → motive t)
  (goal: (t : Nat) → motive t → Prop)
  (h_1 : goal 0 zero)
  (h_2 : (h : t.ctorIdx ≠ 0) → goal t («else» h)) :
  goal t (natToBin3._sparseCasesOn_1 (motive := motive) t zero «else») := by
  unfold _sparseCasesOn_1
  cases t
  · exact h_1
  · apply h_2


theorem natToBin3.match_1.unfold.{u_1}
  (motive : (x : Nat) → Parity x → Sort u_1)
  (alt_1 : (x : Parity 0) → motive 0 x)
  (alt_2 : (j : Nat) → motive (j + j) (Parity.even j))
  (alt_3 : (j : Nat) → motive (j + j).succ (Parity.odd j))
  (goal : (x : Nat) → (p : Parity x) → motive x p → Prop)
  (h_1 : (p : Parity 0) → goal 0 p (alt_1 p))
  (h_2 : (j : Nat) → goal (j + j) (Parity.even j) (alt_2 j))
  (h_3 : (j : Nat) → goal ((j + j).succ) (Parity.odd j) (alt_3 j))
  (n : Nat) (p : Parity n)
  : goal n p (natToBin3.match_1 motive n p alt_1 alt_2 alt_3) := by
  unfold natToBin3.match_1
  revert p
  refine _sparseCasesOn_1.unfold (goal := fun n (r : (p : Parity n) → motive n p) => ∀ p, goal n p (r p)) _ _ _ ?_ ?_
  · intro p
    exact h_1 p
  · intro hne
    intro p
    cases p
    · dsimp
      apply h_2
    · dsimp
      apply h_3


@[elab_as_elim]
theorem natToBin3.match_1.splitting_unfold.{u_1}
  (motive : (x : Nat) → Parity x → Sort u_1)
  (alt_1 : (x : Parity 0) → motive 0 x)
  (alt_2 : (j : Nat) → motive (j + j) (Parity.even j))
  (alt_3 : (j : Nat) → motive (j + j).succ (Parity.odd j))
  (goal : (x : Nat) → (p : Parity x) → motive x p → Prop)
  (h_1 : (p : Parity 0) → goal 0 p (alt_1 p))
  (h_2 :  (j : Nat) → (hnot1 :  ∀ (p : Parity 0), j + j = 0 → Parity.even j ≍ p → False) → goal (j + j) (Parity.even j) (alt_2 j))
  (h_3 : (j : Nat) → goal ((j + j).succ) (Parity.odd j) (alt_3 j))
  (n : Nat) (p : Parity n)
  : goal n p (natToBin3.match_1 motive n p alt_1 alt_2 alt_3) := by
  unfold natToBin3.match_1
  revert p
  refine _sparseCasesOn_1.unfold (goal := fun n (r : (p : Parity n) → motive n p) => ∀ p, goal n p (r p)) _ _ _ ?_ ?_
  · intro p
    exact h_1 p
  · intro hne
    intro p
    cases p
    · dsimp
      apply h_2
      -- solving overlap here, just like for a normal splitter, nothing special
      intros p heq; rw [heq] at hne; contradiction
    · dsimp
      apply h_3

but it doesn’t really help. In order to apply we need to generalize, so we cannot directly apply it to

  (hnot1 :  ∀ (p : Parity 0), j + j = 0 → Parity.even j ≍ p → False) :
  natToBin3.match_1 motive (j + j) (.even j) alt_1 alt_2 alt_3 = alt_2 j := by

but instead have to apply it like this:

theorem natToBin3.match_1.congr_eq1.{u_1}
  (motive : (x : Nat) → Parity x → Sort u_1)
  (alt_1 : (x : Parity 0) → motive 0 x)
  (alt_2 : (j : Nat) → motive (j + j) (Parity.even j))
  (alt_3 : (j : Nat) → motive (j + j).succ (Parity.odd j))
  (j : Nat)
  (hnot1 :  ∀ (p : Parity 0), j + j = 0 → Parity.even j ≍ p → False)
  (n : Nat) (p : Parity n)
  (hn : n = j + j)
  (hp : p ≍ Parity.even j)  :
  natToBin3.match_1 motive n p alt_1 alt_2 alt_3 ≍ alt_2 j := by
  revert hn hp
  refine natToBin3.match_1.splitting_unfold motive alt_1 alt_2 alt_3 _ ?_ ?_ ?_ n p
  · intro p h0j hp
    exfalso
    apply hnot1 p h0j.symm hp.symm
  · intro j' hnot1' hjj' hpp
    sorry -- heq issue!
  · intro j' hjj' hpp
    -- similar
    sorry

and the two sorry cases run into the issue with the heterogeneous equality between the constructors, Parity.even n✝ ≍ Parity.even j. :-(

[Aaron Liu]

Joachim Breitner said:

It seems that Parity.even n✝ ≍ Parity.even j is not good enough to make progress here.

those cases seem solvable to me, but I can't imagine what it would take to automate them

[Joachim Breitner]

Even if we have a possibly non-injective function in the index?
I would assume you’d run into #lean4 > Puzzle: Decidable HEq @ 💬 and then you lost.

[Aaron Liu]

here we go

opaque double : Nat → Nat

inductive Parity : Nat -> Type
| even (n) : Parity (double n)
| odd  (n) : Parity (Nat.succ (double n))

def simple : (n : Nat) → Parity n →  List Bool
| _, Parity.even j => [false, false]
| _, Parity.odd  j => [true, true]

set_option pp.match false

/--
info: private theorem simple.match_1.congr_eq_1.{u_1} : ∀ (motive : (x : Nat) → Parity x → Sort u_1) (x : Nat)
  (x_1 : Parity x) (h_1 : (j : Nat) → motive (double j) (Parity.even j))
  (h_2 : (j : Nat) → motive (double j).succ (Parity.odd j)) (j : Nat),
  x = double j → x_1 ≍ Parity.even j → simple.match_1 motive x x_1 h_1 h_2 ≍ h_1 j
-/
#guard_msgs in
#print sig simple.match_1.congr_eq_1

-- copied from mathlib
theorem congr_heq {α β : Sort u} {γ : Sort v} {f : α → γ} {g : β → γ} {x : α} {y : β}
    (h₁ : f ≍ g) (h₂ : x ≍ y) : f x = g y := by cases h₂; cases h₁; rfl

theorem congr_arg_heq {α : Sort u} {β : α → Sort v} (f : (a : α) → β a)
    {a₁ a₂ : α} : a₁ = a₂ → f a₁ ≍ f a₂ := by intro rfl; rfl

theorem congr_eq_1_by_split : ∀ (motive : (x : Nat) → Parity x → Sort u_1) (x : Nat)
  (x_1 : Parity x) (h_1 : (j : Nat) → motive (double j) (Parity.even j))
  (h_2 : (j : Nat) → motive (double j).succ (Parity.odd j)) (j : Nat),
  x = double j → x_1 ≍ Parity.even j → simple.match_1 motive x x_1 h_1 h_2 ≍ h_1 j := by
  intro motive n p alt1 alt2 j hn hp
  unfold simple.match_1; dsimp
  cases p
  · dsimp
    let f (n : Nat) (x : Parity n) : Nat :=
      x.casesOn (even := id) (odd := id)
    have hf := congr_heq (congr_arg_heq f hn) hp
    cases hf
    rfl
  · dsimp
    let f (n : Nat) (x : Parity n) : Bool :=
      x.casesOn (even := fun _ => true) (odd := fun _ => false)
    have hf := congr_heq (congr_arg_heq f hn) hp
    cases hf

[Joachim Breitner]

Oh, interesting! You can probably use Parity.ctorIdx instead of the local f.

So is ctor1 .. ≍ ctor2 .. → False provable for any two inductive data types ctor1 and ctor2 after all?

[Aaron Liu]

well no

[Aaron Liu]

this is why heq is bad

[Aaron Liu]

I had to use my hn which was lying around

[Aaron Liu]

if you don't know that the indices are equal you can't really do anything

[Joachim Breitner]

Ok, but if you know that the indices are equal (even in the form f n = f n for opaque f) you are good?

[Aaron Liu]

if you know the indices are equal then you're good

[Joachim Breitner]

:thinking:

[Joachim Breitner]

Ok, putting these ideas into the my code above I get (just for reference)

import Lean

inductive Parity : Nat -> Type
| even (n) : Parity (n + n)
| odd  (n) : Parity (Nat.succ (n + n))

partial def natToBin3 : (n : Nat) → Parity n →  List Bool
| 0, _             => []
| _, Parity.even j => [false, false]
| _, Parity.odd  j => [true, true]

-- #check natToBin3.match_1.eq_1

/--
info: natToBin3.match_1.{u_1} (motive : (x : Nat) → Parity x → Sort u_1) (x✝ : Nat) (x✝¹ : Parity x✝)
  (h_1 : (x : Parity 0) → motive 0 x) (h_2 : (j : Nat) → motive (j + j) (Parity.even j))
  (h_3 : (j : Nat) → motive (j + j).succ (Parity.odd j)) : motive x✝ x✝¹
-/
#guard_msgs in
#check natToBin3.match_1

-- #11402
theorem natToBin3._sparseCasesOn_1.else_eq.{u} {motive : Nat → Sort u} (t : Nat) (zero : motive Nat.zero)
  («else»: t.ctorIdx ≠ 0 → motive t) (h : t.ctorIdx ≠ 0) :
  _sparseCasesOn_1 t zero «else» = «else» h := by
  unfold _sparseCasesOn_1
  cases t <;> dsimp
  contradiction

-- fun_cases for sparseCasesOn.
theorem natToBin3._sparseCasesOn_1.unfold.{u}
  {motive : Nat → Sort u} (t : Nat)
  (zero : motive Nat.zero) («else»: t.ctorIdx ≠ 0 → motive t)
  (goal: (t : Nat) → motive t → Prop)
  (h_1 : goal 0 zero)
  (h_2 : (h : t.ctorIdx ≠ 0) → goal t («else» h)) :
  goal t (natToBin3._sparseCasesOn_1 (motive := motive) t zero «else») := by
  unfold _sparseCasesOn_1
  cases t
  · exact h_1
  · apply h_2


theorem natToBin3.match_1.unfold.{u_1}
  (motive : (x : Nat) → Parity x → Sort u_1)
  (alt_1 : (x : Parity 0) → motive 0 x)
  (alt_2 : (j : Nat) → motive (j + j) (Parity.even j))
  (alt_3 : (j : Nat) → motive (j + j).succ (Parity.odd j))
  (goal : (x : Nat) → (p : Parity x) → motive x p → Prop)
  (h_1 : (p : Parity 0) → goal 0 p (alt_1 p))
  (h_2 : (j : Nat) → goal (j + j) (Parity.even j) (alt_2 j))
  (h_3 : (j : Nat) → goal ((j + j).succ) (Parity.odd j) (alt_3 j))
  (n : Nat) (p : Parity n)
  : goal n p (natToBin3.match_1 motive n p alt_1 alt_2 alt_3) := by
  unfold natToBin3.match_1
  revert p
  refine _sparseCasesOn_1.unfold (goal := fun n (r : (p : Parity n) → motive n p) => ∀ p, goal n p (r p)) _ _ _ ?_ ?_
  · intro p
    exact h_1 p
  · intro hne
    intro p
    cases p
    · dsimp
      apply h_2
    · dsimp
      apply h_3


@[elab_as_elim]
theorem natToBin3.match_1.splitting_unfold.{u_1}
  (motive : (x : Nat) → Parity x → Sort u_1)
  (alt_1 : (x : Parity 0) → motive 0 x)
  (alt_2 : (j : Nat) → motive (j + j) (Parity.even j))
  (alt_3 : (j : Nat) → motive (j + j).succ (Parity.odd j))
  (goal : (x : Nat) → (p : Parity x) → motive x p → Prop)
  (h_1 : (p : Parity 0) → goal 0 p (alt_1 p))
  (h_2 :  (j : Nat) → (hnot1 :  ∀ (p : Parity 0), j + j = 0 → Parity.even j ≍ p → False) → goal (j + j) (Parity.even j) (alt_2 j))
  (h_3 : (j : Nat) → goal ((j + j).succ) (Parity.odd j) (alt_3 j))
  (n : Nat) (p : Parity n)
  : goal n p (natToBin3.match_1 motive n p alt_1 alt_2 alt_3) := by
  unfold natToBin3.match_1
  revert p
  refine _sparseCasesOn_1.unfold (goal := fun n (r : (p : Parity n) → motive n p) => ∀ p, goal n p (r p)) _ _ _ ?_ ?_
  · intro p
    exact h_1 p
  · intro hne
    intro p
    cases p
    · dsimp
      apply h_2
      -- solving overlap here, just like for a normal splitter, nothing special
      intros p heq; rw [heq] at hne; contradiction
    · dsimp
      apply h_3

theorem congr_heq {α β : Sort u} {γ : Sort v} {f : α → γ} {g : β → γ} {x : α} {y : β}
    (h₁ : f ≍ g) (h₂ : x ≍ y) : f x = g y := by cases h₂; cases h₁; rfl

theorem congr_arg_heq {α : Sort u} {β : α → Sort v} (f : (a : α) → β a)
    {a₁ a₂ : α} : a₁ = a₂ → f a₁ ≍ f a₂ := by intro rfl; rfl


theorem natToBin3.match_1.congr_eq1.{u_1}
  (motive : (x : Nat) → Parity x → Sort u_1)
  (alt_1 : (x : Parity 0) → motive 0 x)
  (alt_2 : (j : Nat) → motive (j + j) (Parity.even j))
  (alt_3 : (j : Nat) → motive (j + j).succ (Parity.odd j))
  (j : Nat)
  (hnot1 :  ∀ (p : Parity 0), j + j = 0 → Parity.even j ≍ p → False)
  (n : Nat) (p : Parity n)
  (hn : n = j + j)
  (hp : p ≍ Parity.even j)  :
  natToBin3.match_1 motive n p alt_1 alt_2 alt_3 ≍ alt_2 j := by
  revert hn hp
  refine natToBin3.match_1.splitting_unfold motive alt_1 alt_2 alt_3 _ ?_ ?_ ?_ n p
  · intro p h0j hp
    exfalso
    apply hnot1 p h0j.symm hp.symm
  · intro j' hnot1' hjj' hpp
    let get_j (n : Nat) (x : Parity n) : Nat :=
      x.casesOn (even := fun j => j) (odd := fun j => j)
    have hj := congr_heq (congr_arg_heq get_j hjj') hpp
    cases hj
    rfl
  · intro j' hjj' hpp
    have hf := congr_heq (congr_arg_heq (fun n p => p.ctorIdx) hjj') hpp
    contradiction


theorem natToBin3.match_1.eq1.{u_1}
  (motive : (x : Nat) → Parity x → Sort u_1)
  (alt_1 : (x : Parity 0) → motive 0 x)
  (alt_2 : (j : Nat) → motive (j + j) (Parity.even j))
  (alt_3 : (j : Nat) → motive (j + j).succ (Parity.odd j))
  (j : Nat)
  (hnot1 :  ∀ (p : Parity 0), j + j = 0 → Parity.even j ≍ p → False)
  :
  natToBin3.match_1 motive (j + j) (.even j) alt_1 alt_2 alt_3 = alt_2 j := by
  apply eq_of_heq
  apply natToBin3.match_1.congr_eq1 motive alt_1 alt_2 alt_3 j hnot1 <;> rfl

Hmm, this may be doable. Still a very heavy hammer.

[Joachim Breitner]

I assume the point of the let f in the first case is to get out the equalities between the constructor fields, and one would repeat that construct for every field (or at least every field that’s mentioned in the indices)…

[Joachim Breitner]

In light of this encouragement I probably don't need the fun_cases-like lemma, and can just keep splitting the matcher implementation until I hit the branch, and then apply this hypothetical HEq unification tactic

[Joachim Breitner]

Hmm, are we simply missing a HEq variant of the noConfusion principle here, for a more systematic way to take apart heq’s between constructors?

def Parity.hnoConfusion_type (P : Prop) : (n₁ : Nat) → (p₁ : Parity n₁) → (n₂ : Nat) → (p₂ : Parity n₂) → Prop
  | _, Parity.even i, _, Parity.even j => (i = j → P) → P
  | _, Parity.even i, _, Parity.odd j => P
  | _, Parity.odd j, _, Parity.even i => P
  | _, Parity.odd i, _, Parity.odd j => (i = j → P) → P

theorem Parity.hnoConfusion n₁ (p₁ : Parity n₁) n₂ (p₂ : Parity n₂) (hn : n₁ = n₂) (hp : p₁ ≍ p₂) :
    Parity.hnoConfusion_type P n₁ p₁ n₂ p₂ := by
  cases hn; cases hp; cases p₁
  · intro h; apply h; rfl
  · intro h; apply h; rfl

example
  (motive : (x : Nat) → Parity x → Sort u_1)
  (h_2 : (j : Nat) → motive (j + j) (Parity.even j))
  (j n : Nat)
  (heq_1 : n + n = j + j)
  (heq_2 : Parity.even n ≍ Parity.even j):
  h_2 n ≍ h_2 j := by
  apply Parity.hnoConfusion _ _ _ _ heq_1 heq_2
  intro rfl
  rfl

[Joachim Breitner]

I’m inclined to add that construction to Lean (RFC #11450), so that grind can use it to solve examples like above. Having this as a reliable powerful tactic may unblock my equational theorem generation. Thanks for all your input here!

[Notification Bot]

4 messages were moved from this topic to #lean4 > incomplete discriminant refinement procedure by Joachim Breitner.