simp doesn't substitute my definitions

Stream: general

[Igor Ernst]

I'm defining a comm_ring:

add := @add' n
-- ... etc

Then I need to prove stuff like add_zero, add_left_neg, etc.

Here's the error I get:

switched to simple application elaboration procedure because failed to use expected type to elaborate it, error message
type mismatch, term
add_def'' ?m_3 ?m_4
has type
↑(add' ?m_3 ?m_4) = (?m_3.val + ?m_4.val) % ?m_1
but is expected to have type
↑(add_semigroup.add na ⟨a, ha⟩) = ↑0

How can I deal with this?

[Floris van Doorn]

A #mwe would be helpful

[Floris van Doorn]

But it might be the case that the left hand sides will match fine. It's just unlikely that those right hand sides will match. It seems that you have to prove that something equals 0, and add_def'' seems to prove that something is equal to (_ + _) % _

[Igor Ernst]

import data.nat.basic
import tactic

namespace modular

variables {n : nat} [npos : n > 1]

def add' {n} {npos : n > 1} : {k : ℕ // k < n} → {k : ℕ // k < n} → {k : ℕ // k < n} :=
λ a b, match (a,b) with
    | ⟨⟨a₁, ha⟩, ⟨b₁, hb⟩ ⟩ :=
      ⟨
        (a₁ + b₁) % n,
        begin
          apply nat.mod_lt,
          exact nat.lt_of_succ_lt npos,
        end
      ⟩
    end

def neg' {n} {npos : n > 1} : {k : ℕ // k < n} → {k : ℕ // k < n} :=
 λ a, match a with
    | ⟨0, hk⟩ := ⟨0, hk⟩
    | ⟨k + 1, hk⟩ := ⟨n - k - 1,
      begin
        show n - (k + 1) < n,
        apply (nat.sub_lt_left_iff_lt_add (by {exact le_of_lt hk} : (k+ 1) ≤ n)).2,
        simp only [nat.succ_pos', lt_add_iff_pos_left],
      end⟩
      end

@[simp]
lemma neg_prop : ∀ a ha, (@neg' n npos ⟨a,ha⟩).1 % n = (n - a) % n :=
begin
  intros,
  simp,
  induction a,
  {
    have h : neg' ⟨0, ha⟩ = ⟨0, ha⟩, by refl,
    rw h,
    simp,
  },
  {
    have h : ↑ (neg' ⟨a_n + 1, ha⟩ ) = n - a_n - 1, by {simp,refl},
    rw h,
    refl,
  }
end

@[simp]
lemma add_def': ∀ a {ha} b {hb}, ↑(@add' n npos ⟨a, ha⟩ ⟨b, hb⟩) = (a + b) % n :=
begin
  intros a ha b hb,
  refl,
end

@[simp]
lemma add_def'' : ∀ a b, ↑(@add' n npos a b) = (a.1 + b.1) % n :=
begin
  rintros ⟨a, ha⟩ ⟨b, hb⟩,
  refl,
end


def modN [npos : n > 1] : comm_ring {k : ℕ // k < n} :=
{ add := @add' n npos,
  add_assoc :=
    begin
      rintros ⟨a,ha⟩ ⟨b,hb⟩ ⟨c,hc⟩,
      ext,
      simp,
      ring,
    end,
  zero := ⟨0, by {linarith}⟩,
  zero_add :=
    begin
      rintro ⟨a, ha⟩,
      ext,
      unfold has_add.add,
      simp,
      exact nat.mod_eq_of_lt ha,
    end,
  add_zero :=
    begin
      rintro ⟨a, ha⟩,
      ext,
      unfold has_add.add,
      simp,
      exact nat.mod_eq_of_lt ha,
    end,
  neg := @neg' n npos,
  add_left_neg :=
    begin
      rintro ⟨ a, ha⟩ ,
      ext,
      unfold has_neg.neg,
      unfold has_add.add,
      simp,
      set na := @neg' n npos ⟨a,ha⟩ with hna,
      refine add_def'' na ⟨a,ha⟩, -- problem is here
      simp [add_def''],
      refl,
    end,
  add_comm := _,
  mul := _,
  mul_assoc := _,
  one := _,
  one_mul := _,
  mul_one := _,
  left_distrib := _,
  right_distrib := _,
  mul_comm := _ }

[Floris van Doorn]

I'm getting a bunch of errors in your file. But I think the relevant error can be solved as follows: refine (@add_def'' n npos na ⟨a,ha⟩).trans _,

[Floris van Doorn]

Taking a step back, it might be useful (albeit verbose) to state all comm_ring fields as lemmas about add' and then you can write
add_left_neg := my_add_left_neg where my_add_left_neg will have type ∀ (a : {k // k < n}), add' (-a) a = 0

[Floris van Doorn]

You can also use change ∀ (a : {k // k < n}), @add' n npos (@neg' n npos a) a = _, as the first tactic in that block to manually unfold.

[Floris van Doorn]

You might also want to start your file with

variables {n : ℕ} [npos : fact (n > 1)]
include npos

(and then not redeclare n/npos again in lemmas). This means that n and npos will be found my Lean automatically (assuming enough type information is around)

[Igor Ernst]

Very helpful, thanks a lot