Remembering the state in a pattern matching

Stream: new members

[Mukesh Tiwari]

Hi everyone, how can I discharge the two admits in the theorem int_to_nat_injective? I am looking for a tactics that remembers the state , i.e., in the first case it should be Ha : n % 2 == 0 = false and in the second case it should be Ha : n % 2 == 0 = true.

section cantor


  def nat_to_int : Nat -> Int :=
    fun n =>
    match n % 2 == 0 with
    | true => n / 2
    | false => - (n + 1) / 2


  def int_to_nat : Int -> Nat
  | Int.ofNat n => 2 * n
  | Int.negSucc n => 2 * n + 1


  #eval nat_to_int (int_to_nat (-700))
  #eval int_to_nat (nat_to_int 3)

  theorem nat_to_int_injective : ∀ (n : Int),
    nat_to_int (int_to_nat n) = n := by
    intro n
    rcases n with n | n; simp
    . simp [nat_to_int, int_to_nat]
    . simp [int_to_nat, nat_to_int]
      have Ha : (2 * n + 1) % 2 = 1 := by omega
      simp [Ha]
      have Hb : -(2 * ↑n + 1 + 1) / 2 = Int.negSucc ((2 * n + 1) / 2) := by
        exact rfl
      rw [Hb]; simp; omega




  theorem int_to_nat_injective : ∀ (n : Nat),
    int_to_nat (nat_to_int n) = n := by
    intro n
    simp [int_to_nat, nat_to_int]
    rcases n % 2 == 0 with _ | _; simp
    . have Ha : -(↑n + 1) / 2 = Int.negSucc (n / 2) := by exact rfl
      rw [Ha]; simp
      /- I know that n is odd here -/
      admit
    . have Ha : ↑n / 2 = Int.ofNat (n / 2) := by exact rfl
      rw [Ha]; simp
      /- I know n is even here -/
      admit

[Logan Murphy]

In your case analysis, you can name the hypothesis: rcases h: n % 2 == 0 with _ | _; simp . Is that what you need?

[Mukesh Tiwari]

Thank you! That's what I need.

[Mukesh Tiwari]

I have another question. How to tell the Lean type checker that termination argument is (a + b)?

  def gcd_proof : Nat -> Nat -> Nat := by
    intro a b
    rcases ha : a with _ | ar
    . exact b
    . rcases hb : b with _ | br
      . exact a
      . refine' (if hc : a < b then _ else _)
        . have hd : a + (b % a) < a + b  := by sorry
          exact (gcd_proof a (b % a))
        . have hd : (a % b) + b < a + b := by sorry
          exact (gcd_proof (a % b) b)


fail to show termination for
  gcd_proof
with errors
argument #1 was not used for structural recursion
  failed to eliminate recursive application
    gcd_proof a (b % a)

argument #2 was not used for structural recursion
  failed to eliminate recursive application
    gcd_proof a (b % a)

[Mario Carneiro]

termination_by a b => a + b

[Mukesh Tiwari]

Thanks! Now that you are here, how can I replace the sorry part in have hd : a + (b % a) < a + b := by sorry by a proof (omega is not able to solve it)?

[Mario Carneiro]

Nat.mod_lt b a and then omega should do the trick