Best way to prove that `A 1` is empty in this example?

Stream: new members

[Yongyi Chen]

import Mathlib

inductive A : ℕ → Type
| base : A 6
| double : A m → A (2 * m)
| half : A (2 * m) → A m

theorem noA_attempt1 : A 1 → False := by
  intro a
  /-
  tactic 'cases' failed, nested error:
  dependent elimination failed, failed to solve equation
    1 = Nat.mul 2 m✝
  at case @A.double after processing
    _
  the dependent pattern matcher can solve the following kinds of equations
  - <var> = <term> and <term> = <var>
  - <term> = <term> where the terms are definitionally equal
  - <constructor> = <constructor>, examples: List.cons x xs = List.cons y ys, and List.cons x xs = List.nil
  -/
  match a with
  | .half (a : A 2) => sorry

theorem noA_attempt2 : A 1 → False := by
  intro a
  /-
  dependent elimination failed, failed to solve equation
    1 = Nat.mul 2 m✝
  -/
  cases a with
  | half a => sorry

theorem noA_attempt3 : A 1 → False := by
  intro a
  /-
  index in target's type is not a variable (consider using the `cases` tactic instead)
    1
  -/
  induction a with
  | base => sorry
  | double _ _ => sorry
  | half _ _ => sorry

theorem noA_attempt4 : A 1 → False := by
  intro a
  generalize h : 1 = x at a
  induction a with
  | base => contradiction
  | double _ _ =>
    have : 2 ∣ 1 := Dvd.intro _ h.symm
    contradiction
  | half a ih =>
    subst h
    /-
    case half
    x : ℕ
    a : A (2 * 1)
    ih : 1 = 2 * 1 → False
    ⊢ False
    -/
    sorry
    -- Looks like I have to prove A 2 is empty. But in doing that I will need
    -- to prove A 1 is empty. Circular dependency...

I posted this here because I think there is possibly some tactic or variation of these tactics I am not aware of to solve this.

[Yongyi Chen]

In this example I can conceive of proving that A n is empty whenever n is not 3 times a power of 2. However this is just an MWE and in the actual use case, it is difficult to generalize the condition like that. I am also interested in knowing whether generalize h : 1 = x at a followed by induction a is indeed the only cases-like tactic that can be used without errors for things like this. As you can see, I kept encountering dependent elimination failed errors with with match and cases.

[Yongyi Chen]

OK, I realize that this particular MWE most likely requires something mathematical to be done to achieve the proof, which makes this not a particularly good example for what I'm trying to ask. Maybe a better example is:

inductive B : ℕ → Type
| step1 : B 2 → B 5
| step2 : B 5 → B 8
| step3 : B 8 → B 2

theorem noB : B 2 → False := by
  sorry

[Yongyi Chen]

OK, here's a solution:

theorem noB : B 2 → False := by
  intro b
  generalize h : 2 = x at b
  have h' : x = 2 ∨ x = 5 ∨ x = 8 := Or.inl h.symm
  clear h
  induction b <;> simp_all

Is there a shorter one? And my original question (proving that A 1 is empty) still stands.

[Yongyi Chen]

Another way:

mutual
theorem noB2 : B 2 → False
| B.step3 b => noB8 b

theorem noB5 : B 5 → False
| .step1 b => noB2 b

theorem noB8 : B 8 → False
| .step2 b => noB5 b
end

I don't understand why, but if B's target type is changed from Type to Prop, this solution doesn't work anymore.

[Yuyang Zhao]

My solution:

import Mathlib

inductive A : ℕ → Type
| base : A 6
| double : A m → A (2 * m)
| half : A (2 * m) → A m

lemma noA : A n → (∃ k, n = 2 ^ k) → False := by
  intro a
  induction a with
  | base =>
    rintro ⟨k, hk⟩
    match k with
    | 0 | 1 => norm_num at hk
    | k + 2 =>
      simp [pow_succ, ← mul_assoc] at hk
      norm_num at hk
      have : (4 : ℕ) ∣ 6 := ⟨2 ^ k, hk⟩
      norm_num at this
  | double _ ih =>
    rintro ⟨k, hk⟩
    cases' k with k
    · simp at hk
    · simp [pow_succ] at hk
      exact ih ⟨k, hk⟩
  | half a ih =>
    rintro ⟨k, rfl⟩
    apply ih
    exact ⟨k + 1, (pow_succ _ _).symm⟩

example : A 1 → False := (noA · ⟨0, rfl⟩)