Include in proof context the patterns that didn't match?

Stream: new members

[George Zakhour]

Hey everyone :)

Setup

I have an inductive type (call it T) with a lot of constructors, let's call them K1 up to Kn.

I have a proposition (P : T -> Prop) that I am proving by case analysis on T without using tactics.
Basically I have something that looks like this:

theorem thm (e: T) : P e :=
  match e with
  | K1 _ => ...
  ...
  | Kn => ...

Now I happen to know that for a large majority of these constructors, P holds "trivially" (i.e. with not a lot of code) and that the mess is really in the first 3 constructors.

So ideally I would love to write

theorem thm (e: T) : P e :=
  match e with
  | K1 => ...
  | K2 => ...
  | K3 => ...
  | _ => trivial

Problem

I lose the fact that e = K4 \or e = K5 \or ... \or e = Kn which is the only way to make progress in my proof. I know I could write

match e with
...
| K4 | K5 | K6 | ... | Kn => all_goals (trivial)

but I would love not having to enumerate all the remaining constructors.

Question

Any way I can get information about which patterns an expression didn't match in my proof context so I can use it?

I appreciate any help!

[Aaron Liu]

theorem thm (e: T) : P e := by
  cases e with
  | K1 => ...
  | K2 => ...
  | K3 => ...
  | _ => trivial

[George Zakhour]

But I do not have in my context e = K4 \or e = K5 \or ... \or e = Kn in the branch with the wildcard. I can't make progress on my proof without this hypothesis.

[Aaron Liu]

In the branch with the wildcard, you should be working on the cases K4, K5, ..., Kn simultaneously.

[Aaron Liu]

This is the same as

match e with
...
| K4 | K5 | K6 | ... | Kn => all_goals (trivial)

but without needing to enumerate all the remaining constructors.

[George Zakhour]

yes I know this, but in the proof context I don't know this.

Maybe i miscommunicated, but the proof term in the last branch isn't exactly the tactic trivial.
It's a placeholder for some expression in which I need to use the fact that e = K4 \or ... \or e = Kn if I want to finish the proof.

[Aaron Liu]

You will need to provide more details for me to help you more.

[George Zakhour]

I appreciate your help, I will try to minimize my case and paste it here and I hope it won't be a wall of text.

IG is my inductive type with 5 constructors.

I am trying to prove a lemma on two values of IG. I happen to know that it's symmetric and I really want to avoid duplicating parts of the proof.

I hope you can see that the pattern matches after -- symmetric cases look obnoxious, and if I can collapse them under a wildcard that'd be ideal.

The problem is that if I do so, I lose the possibilities for g1 and g2 and i cannot use that to say that they violate ord_cond

@[simp]
def constructor_num {α: Type} (g: IG) : Nat := match g with
  | IG.Empty => 0
  | IG.Add _ _ => 1
  | IG.Remove _ _ => 2
  | IG.Connect _ _ _ => 3
  | IG.Disconnect _ _ _ => 4


theorem symmetric_lemma {α: Type}
  (g1 g2: IG)
  (ord_cond: constructor_num g1 <= constructor_num g2)
  (cond: ⟦g1⟧ = ⟦g2⟧)
  : g1 ≃ g2
  := match case: (g1, g2) with
    | ⟨IG.Empty, IG.Empty⟩ => sorry
    | ⟨IG.Empty, IG.Add a g⟩ => sorry
    | ⟨IG.Empty, IG.Remove a g⟩ => sorry
    | ⟨IG.Empty, IG.Connect a b g⟩ => sorry
    | ⟨IG.Empty, IG.Disconnect a b g⟩ => sorry
    | ⟨IG.Add a g1, IG.Add b g2⟩ => sorry
    | ⟨IG.Add a g1, IG.Remove b g2⟩ => sorry
    | ⟨IG.Add a g1, IG.Connect b c g2⟩ => sorry
    | ⟨IG.Add a g1, IG.Disconnect b c g2⟩ => sorry
    | ⟨IG.Remove a g1, IG.Remove b g2⟩ => sorry
    | ⟨IG.Remove a g1, IG.Connect b c g2⟩ => sorry
    | ⟨IG.Remove a g1, IG.Disconnect b c g2⟩ => sorry
    | ⟨IG.Connect a b g1, IG.Connect c d g2⟩ => sorry
    | ⟨IG.Connect a b g1, IG.Disconnect c d g2⟩ => sorry
    | ⟨IG.Disconnect a b g1, IG.Disconnect c d g2⟩ => sorry

    --  symmetric cases
    | ⟨IG.Add _ _, IG.Empty⟩ | ⟨IG.Remove _ _, IG.Empty⟩ | ⟨IG.Remove _ _, IG.Add _ _⟩
    | ⟨IG.Connect _ _ _, IG.Empty⟩ | ⟨IG.Connect _ _ _, IG.Add _ _⟩ | ⟨IG.Connect _ _ _, IG.Remove _ _⟩
    | ⟨IG.Disconnect _ _ _, IG.Connect _ _ _⟩
    | ⟨IG.Disconnect _ _ _, IG.Remove _ _⟩ | ⟨IG.Disconnect _ _ _, IG.Add _ _⟩
    | ⟨IG.Disconnect _ _ _, IG.Empty⟩ => by all_goals (simp at case; simp [case] at ord_cond)


theorem lemma
  : ∀ (g1 g2: IG), ⟦g1⟧ = ⟦g2⟧ → g1 ≃ g2
  := by
    intros g1 g2 cond
    by_cases ord_cond: constructor_num g1 < constructor_num g2
    . exact lemma_equiv_rules_complete g1 g2 (Nat.le_of_lt ord_cond) cond
    . exact Equiv.Symm $ symmetric_lemma g2 g1 (Nat.le_of_not_lt ord_cond) (by simp [cond])

I hope that helps in clarifying my need

[Aaron Liu]

You can do cases on g1, and then do cases on g2