How to prove basic lemma involving quotients

Stream: new members

[Matei Adriel]

In particular, I want to prove:

  def negate (τ: MyInt): MyInt :=
    Quot.liftOn τ negateRawInt @negateRawInt.respects

  private theorem double_neg_elim: ∀x, x = negate (negate x) := by
    intro x
    sorry

The full file can be found here

[Kyle Miller]

  private theorem raw_int_double_neg_elim: ∀x, x = negate (negate x) := by
    intro x
    induction x using Quot.ind with
    | mk x' =>
      cases x'
      rfl

[Kyle Miller]

If your theorem starts with intro, you can put the universally quantified variable before the colon. You can also take advantage of a feature to reduce indentation here:

  private theorem raw_int_double_neg_elim (x : MyInt) : x = negate (negate x) := by
    induction x using Quot.ind with | mk x' =>
    cases x'
    rfl

[Matei Adriel]

Oh, that's so cool! Is there a reference on where I can use the induction tactic? @Kyle Miller

[Kyle Miller]

I'm not sure where documentation for it is. I can give you a rule of thumb, though, for how to use it. You want to give it a function that's a recursor of some sort (one of its arguments is a "motive", and one of its arguments is the thing being inducted on (the "major premise")). Then each case is supposed to match the name of one of the arguments to the recursor (the "minor premises").

For Quot.ind, I happen to know that the name of the minor premise is mk. In the following, β is the motive and q is the major premise.

Quot.ind : ∀ {α : Sort _} {r : α → α → Prop} {β : Quot r → Prop},
  (mk : ∀ (a : α), β (Quot.mk r a)) → ∀ (q : Quot r), β q

[Kyle Miller]

Another example: when you do induction n for n : Nat, my understanding is that it is equivalent do doing induction n using Nat.rec. Then, looking at the type of this recursor,

Nat.rec : {motive : Nat → Sort _} →
  (zero : motive Nat.zero) → (succ : (n : Nat) → motive n → motive (Nat.succ n)) →
  (t : Nat) → motive t

this means induction should follow the form

induction n with
| zero => ...
| succ n ih => ...

where ih : motive n is the induction hypothesis. (I got the type of Nat.rec from #print Nat.rec and then filling in argument names using the names of the constructors for Nat.)

[Kyle Miller]

I'm not actually sure how to check, from within Lean, what the names of the minor hypotheses are supposed to be. When you do #print Quot.ind it doesn't tell you about mk.

[Matei Adriel]

@Kyle Miller so how do I use the induction syntax with Quot.ind\2 ?