Naïve question on induction

Stream: lean4

[Shaopeng]

I am working on a proof by induction on the cardinality of a Finite type. For some reason I get stuck in the base case at what seems to be a grammar/syntax problem. Could someone give me a quick help? The problem is minimized as below with the question in the comments. Any help would be much appreciated!

import Mathlib.SetTheory.Cardinal.Finite
import Mathlib.Data.Finite.Card
set_option linter.unusedVariables false

open Finite
lemma isEmpty_maps_equal2 {β : Type _}{h0 : IsEmpty β}{M: Type _}
  (v1: β → M)(v2: β → M) : v1 = v2 :=
  have prf: (∀ (x:β), v1 x = v2 x) :=
    fun x => @IsEmpty.elim β h0 (fun x => v1 x = v2 x) x
  funext prf

lemma isEmpty_of_card_zero {β : Type _}{h0 : Nat.card β = 0}[e: Finite β] : IsEmpty β := by
  rw [@card_eq_zero_iff β e] at h0
  exact h0

/-A simplified stmt just to illustrate my question / confusion  on the base case-/
lemma equalVarFinSameEval (β : Type ut)[e: Finite β](M: Type wt)
  (v w: β → M) : v = w := by
  induction (Nat.card β)
  case zero := by
            apply isEmpty_maps_equal2 v w
            apply isEmpty_of_card_zero
            /- Question: At this point the goal is Nat.card β = 0,
               which should be in the scope since we are in the `case zero`.
               However I don't see a `zero: Nat.card β = 0` nor can I use
               `exact zero` or `rfl Nat.zero` etc. to close the case.
               Could you let me know what I am missing? -/
            sorry
  case succ n j := by sorry
            /- this case is incorrect as written, just to focus on the above. -/

[Giacomo Stevanato]

You can do this with cases:

import Mathlib.SetTheory.Cardinal.Finite
import Mathlib.Data.Finite.Card
set_option linter.unusedVariables false

open Finite
lemma isEmpty_maps_equal2 {β : Type _}{h0 : IsEmpty β}{M: Type _}
  (v1: β → M)(v2: β → M) : v1 = v2 :=
  have prf: (∀ (x:β), v1 x = v2 x) :=
    fun x => @IsEmpty.elim β h0 (fun x => v1 x = v2 x) x
  funext prf

lemma isEmpty_of_card_zero {β : Type _}{h0 : Nat.card β = 0}[e: Finite β] : IsEmpty β := by
  rw [@card_eq_zero_iff β e] at h0
  exact h0

/-A simplified stmt just to illustrate my question / confusion  on the base case-/
lemma equalVarFinSameEval (β : Type ut)[e: Finite β](M: Type wt)
  (v w: β → M) : v = w := by
  cases h : (Nat.card β)
  case zero := by
            apply isEmpty_maps_equal2 v w
            apply isEmpty_of_card_zero
            /- Question: At this point the goal is Nat.card β = 0,
               which should be in the scope since we are in the `case zero`.
               However I don't see a `zero: Nat.card β = 0` nor can I use
               `exact zero` or `rfl Nat.zero` etc. to close the case.
               Could you let me know what I am missing? -/
            exact h
  case succ n := by sorry
            /- this case is incorrect as written, just to focus on the above. -/

Notice the h : right after cases, that's the name that will be given to the hypothesis that Nat.card β is equal to the value of the case.

Of course this is not induction, because with induction you can't assume that the inductive variable is equal to Nat.card β for the original β.

[James Sully]

You can also reorder things a bit. induction will rewrite occurrences of the thing you're doing induction on in the goal

  apply isEmpty_maps_equal2 v w
  apply isEmpty_of_card_zero
  -- Goal: ⊢ Nat.card β = 0
  induction (Nat.card β)
  case zero := by
    -- Goal: ⊢ 0 = 0
    rfl

[Shaopeng]

James Sully said:

You can also reorder things a bit. induction will rewrite occurrences of the thing you're doing induction on in the goal

  apply isEmpty_maps_equal2 v w
  apply isEmpty_of_card_zero
  -- Goal: ⊢ Nat.card β = 0
  induction (Nat.card β)
  case zero := by
    -- Goal: ⊢ 0 = 0
    rfl

Thanks, James. I think this works for the case 0 but in the case succ it turns the goal to n + 1 = 0.

[James Sully]

Ah, sorry, I didn't think about this carefully enough

[Shaopeng]

Thank you, Giacomo Stevanato . On that note, if I want to use true induction when proving the case succ i.e.
having at hand the hypothesis that "v = w" holds for smaller cardinalities, I should probably
change the statement to something like

lemma equalVarFinSameEval2 (β : Type ut)[e: Finite β](M: Type wt)
  (v w: β → M) /- (Other variables / conditions) -/
  : (∀ n, n = Nat.card β → v = w) := by sorry

[Shaopeng]

James Sully No problem and thanks a lot for the discussion, James.

[Giacomo Stevanato]

Shaopeng said:

Thank you, Giacomo Stevanato . On that note, if I want to use true induction when proving the case succ i.e.
having at hand the hypothesis that "v = w" holds for smaller cardinalities, I should probably
change the statement to something like

lemma equalVarFinSameEval2 (β : Type ut)[e: Finite β](M: Type wt)
  (v w: β → M) /- (Other variables / conditions) -/
  : (∀ n, n = Nat.card β → v = w) := by sorry

I don't think that statement will be what you want, as v and w are still defined with the outer β.

That said I don't think your lemma is true for any β whose cardinality is not 0, as you could have v := fun _ => 0 and w := fun _ => 1 and they would obviously be distinguishable if there exist a valid input (i.e. the cardinality is not 0) to call them and observe the different output.

[Shaopeng]

Giacomo Stevanato said:

Shaopeng said:

Thank you, Giacomo Stevanato . On that note, if I want to use true induction when proving the case succ i.e.
having at hand the hypothesis that "v = w" holds for smaller cardinalities, I should probably
change the statement to something like

lemma equalVarFinSameEval2 (β : Type ut)[e: Finite β](M: Type wt)
  (v w: β → M) /- (Other variables / conditions) -/
  : (∀ n, n = Nat.card β → v = w) := by sorry

I don't think that statement will be what you want, as v and w are still defined with the outer β.

That said I don't think your lemma is true for any β whose cardinality is not 0, as you could have v := fun _ => 0 and w := fun _ => 1 and they would obviously be distinguishable if there exist a valid input (i.e. the cardinality is not 0) to call them and observe the different output.

Thank you, Giacomo. Yes the lemma as stated is incorrect (there are some other conditions on v and w which I omitted from the statement). Will follow up and filling in the /-(Other variables / conditions) -/ part here if need be.

I agree quantifying over n probably does not give what I want as you pointed out. Might have to try quantifying over β as well, or inducting on something else..