equation compiler help me plz

Stream: general

[Johan Commelin]

import category_theory.preadditive
import category_theory.abelian.projective
import tactic.interval_cases


noncomputable theory

open category_theory
open category_theory.limits

universe variables v u

namespace category_theory

variables {C : Type u} [category.{v} C]

variables (F : fin 4 → C) (a : F 0 ⟶ F 1) (b : F 1 ⟶ F 2) (c : F 2 ⟶ F 3)

namespace fin4_functor_mk

def map : Π (i j : fin 4) (hij : i ≤ j), F i ⟶ F j
| ⟨0,hi⟩ ⟨0,hj⟩ _ := 𝟙 _
| ⟨1,hi⟩ ⟨1,hj⟩ _ := 𝟙 _
| ⟨2,hi⟩ ⟨2,hj⟩ _ := 𝟙 _
| ⟨3,hi⟩ ⟨3,hj⟩ _ := 𝟙 _
| ⟨0,hi⟩ ⟨1,hj⟩ _ := a
| ⟨1,hi⟩ ⟨2,hj⟩ _ := b
| ⟨2,hi⟩ ⟨3,hj⟩ _ := c
| ⟨0,hi⟩ ⟨2,hj⟩ _ := a ≫ b
| ⟨1,hi⟩ ⟨3,hj⟩ _ := b ≫ c
| ⟨0,hi⟩ ⟨3,hj⟩ _ := a ≫ b ≫ c
-- how do I tell Lean that I'm done?

end fin4_functor_mk

def fin4_functor_mk : fin 4 ⥤ C :=
{ obj := F,
  map := _,
  map_id' := _,
  map_comp' := _ }

end category_theory

[Eric Wieser]

def map : Π (i j : fin 4) (hij : i ≤ j), F i ⟶ F j
| ⟨0,hi⟩ ⟨0,hj⟩ _ := 𝟙 _
| ⟨1,hi⟩ ⟨1,hj⟩ _ := 𝟙 _
| ⟨2,hi⟩ ⟨2,hj⟩ _ := 𝟙 _
| ⟨3,hi⟩ ⟨3,hj⟩ _ := 𝟙 _
| ⟨0,hi⟩ ⟨1,hj⟩ _ := a
| ⟨1,hi⟩ ⟨2,hj⟩ _ := b
| ⟨2,hi⟩ ⟨3,hj⟩ _ := c
| ⟨0,hi⟩ ⟨2,hj⟩ _ := a ≫ b
| ⟨1,hi⟩ ⟨3,hj⟩ _ := b ≫ c
| ⟨0,hi⟩ ⟨3,hj⟩ _ := a ≫ b ≫ c
-- oh boy
| ⟨1,hi⟩ ⟨0,hj⟩ h := false.elim $ by linarith [subtype.coe_le_coe.mpr h]
| ⟨2,hi⟩ ⟨0,hj⟩ h := false.elim $ by linarith [subtype.coe_le_coe.mpr h]
| ⟨3,hi⟩ ⟨0,hj⟩ h := false.elim $ by linarith [subtype.coe_le_coe.mpr h]
| ⟨2,hi⟩ ⟨1,hj⟩ h := false.elim $ by linarith [subtype.coe_le_coe.mpr h]
| ⟨3,hi⟩ ⟨1,hj⟩ h := false.elim $ by linarith [subtype.coe_le_coe.mpr h]
| ⟨3,hi⟩ ⟨2,hj⟩ h := false.elim $ by linarith [subtype.coe_le_coe.mpr h]
| ⟨0,hi⟩ ⟨n+4,hj⟩ _ := false.elim $ by linarith
| ⟨1,hi⟩ ⟨n+4,hj⟩ _ := false.elim $ by linarith
| ⟨2,hi⟩ ⟨n+4,hj⟩ _ := false.elim $ by linarith
| ⟨3,hi⟩ ⟨n+4,hj⟩ _ := false.elim $ by linarith
| ⟨n+4,hi⟩ _ _ := false.elim $ by linarith

[Eric Wieser]

Not exactly satisfying

[David Wärn]

MWE:

example : Π n : ℕ, n ≤ 1 → true
| 0 _ := trivial
| 1 _ := trivial
-- non-exhaustive match, the following cases are missing:
-- _example (nat.succ _).succ _

I'm not sure this is a job for the equation compiler?

[Johan Commelin]

This is what I have now:

def map' : Π (i j : fin 4) (hij : i ≤ j), F i ⟶ F j
| ⟨0,hi⟩ ⟨0,hj⟩ _ := 𝟙 _
| ⟨1,hi⟩ ⟨1,hj⟩ _ := 𝟙 _
| ⟨2,hi⟩ ⟨2,hj⟩ _ := 𝟙 _
| ⟨3,hi⟩ ⟨3,hj⟩ _ := 𝟙 _
| ⟨0,hi⟩ ⟨1,hj⟩ _ := a
| ⟨1,hi⟩ ⟨2,hj⟩ _ := b
| ⟨2,hi⟩ ⟨3,hj⟩ _ := c
| ⟨0,hi⟩ ⟨2,hj⟩ _ := a ≫ b
| ⟨1,hi⟩ ⟨3,hj⟩ _ := b ≫ c
| ⟨0,hi⟩ ⟨3,hj⟩ _ := a ≫ b ≫ c
| ⟨i+4,hi⟩ _ _ := by { exfalso, revert hi, dec_trivial }
| _ ⟨j+4,hj⟩ _ := by { exfalso, revert hj, dec_trivial }
| ⟨i+1,hi⟩ ⟨0,hj⟩ H := by { exfalso, revert H, dec_trivial }
| ⟨i+2,hi⟩ ⟨1,hj⟩ H := by { exfalso, revert H, dec_trivial }
| ⟨3,hi⟩ ⟨2,hj⟩ H := by { exfalso, revert H, dec_trivial }

[Johan Commelin]

Accompanied by

lemma map'_id : ∀ (i : fin 4), map' F a b c i i le_rfl = 𝟙 _
| ⟨0,hi⟩ := rfl
| ⟨1,hi⟩ := rfl
| ⟨2,hi⟩ := rfl
| ⟨3,hi⟩ := rfl
| ⟨i+4,hi⟩ := by { exfalso, revert hi, dec_trivial }

def map'_comp : Π (i j k : fin 4) (hij : i ≤ j) (hjk : j ≤ k),
  map' F a b c i j hij ≫ map' F a b c j k hjk = map' F a b c i k (hij.trans hjk)
| ⟨0, _⟩ ⟨0, _⟩ k _ _ := category.id_comp _
| ⟨1, _⟩ ⟨1, _⟩ k _ _ := category.id_comp _
| ⟨2, _⟩ ⟨2, _⟩ k _ _ := category.id_comp _
| i ⟨1, _⟩ ⟨1, _⟩ _ _ := category.comp_id _
| i ⟨2, _⟩ ⟨2, _⟩ _ _ := category.comp_id _
| i ⟨3, _⟩ ⟨3, _⟩ _ _ := category.comp_id _
| ⟨0, _⟩ ⟨1, _⟩ ⟨2, _⟩ _ _ := rfl
| ⟨0, _⟩ ⟨1, _⟩ ⟨3, _⟩ _ _ := rfl
| ⟨0, _⟩ ⟨2, _⟩ ⟨3, _⟩ _ _ := category.assoc a b c
| ⟨1, _⟩ ⟨2, _⟩ ⟨3, _⟩ _ _ := rfl
| ⟨i+4,hi⟩ _ _ _ _ := by { exfalso, revert hi, dec_trivial }
| _ ⟨j+4,hj⟩ _ _ _ := by { exfalso, revert hj, dec_trivial }
| _ _ ⟨k+4,hk⟩ _ _ := by { exfalso, revert hk, dec_trivial }
| ⟨i+1,hi⟩ ⟨0,hj⟩ _ H _ := by { exfalso, revert H, dec_trivial }
| ⟨i+2,hi⟩ ⟨1,hj⟩ _ H _ := by { exfalso, revert H, dec_trivial }
| ⟨3,hi⟩ ⟨2,hj⟩ _ H _ := by { exfalso, revert H, dec_trivial }
| _ ⟨i+1,hi⟩ ⟨0,hj⟩ _ H := by { exfalso, revert H, dec_trivial }
| _ ⟨i+2,hi⟩ ⟨1,hj⟩ _ H := by { exfalso, revert H, dec_trivial }
| _ ⟨3,hi⟩ ⟨2,hj⟩ _ H := by { exfalso, revert H, dec_trivial }

[Eric Wieser]

David Wärn said:

MWE:

example : Π n : ℕ, n ≤ 1 → true
| 0 _ := trivial
| 1 _ := trivial
-- non-exhaustive match, the following cases are missing:
-- _example (nat.succ _).succ _

I'm not sure this is a job for the equation compiler?

For this specific case I feel like it should be, since the proof is simply by-cases:

example : Π n : ℕ, n ≤ 1 → true
| 0 _ := trivial
| 1 _ := trivial
-- there is no `h` that can fill this gap, but we still have to case it ourselves
| (n + 2) (nat.less_than_or_equal.step h) := false.elim $ match h with end

[David Wärn]

Note that this one works:

example : Π n : ℕ, n ≤ 0 → true
| 0 _ := trivial

[David Wärn]

I mean using exfalso like this makes sense, but I'm curious about which absurd patterns the equation compiler can spot on its own

[David Wärn]

Surely when your goal is a Prop you don't have to do this manual case-splitting, there should be some short tactic script which does it for you

[Alex J. Best]

When the goal is a prop there is tactic#fin_cases and tactic#interval_cases:

import tactic
example : Π n : ℕ, n ≤ 1 → true:=
begin
intros n hn,
interval_cases n,
end

Johan's map' isn't a Prop though, but I guess map'_comp is?

[Johan Commelin]

Aah, so I could use fin_cases for map'_comp.

[Yaël Dillies]

Btw #7987 will buff fin_cases by allowing it to work for fin n (and other stuff you can think of).

[Eric Wieser]

Doesn't it already work for fin n?

[Yaël Dillies]

I think not? At least I'm adding the stuff that's needed for it, but it already works using something else?

[Scott Morrison]

The tests for fin_cases says it works on fin n. In fact, the reason it's called fin_cases is the initial implementation only worked on fin n, rather than most finite stuff.

[Scott Morrison]

Regarding the restriction that the target is Prop: we can easily drop this by allowing the tactics to be nonconstructive, and I think we should do this.

[Scott Morrison]

Anytime you get a "can only eliminate into Prop" error, you always have the option of calling nonempty.some first:

noncomputable example (f : ℕ → Type) (p : fin 1) (h0 : f 0) (h1 : f 1) (h2 : f 2) : f 0 :=
begin
  -- Fails with `induction tactic failed, recursor 'or.dcases_on' can only eliminate into Prop`:
  -- fin_cases p,

  -- So try harder:
  apply nonempty.some,
  fin_cases p,
  split,
  assumption,
end

[Scott Morrison]

Given how resolutely classical mathlib is at this point, I think there's little point in our tactics being cautious about this.

[Scott Morrison]

(We could also try to make fin_cases work constructively!)

[Mario Carneiro]

I don't know whether this technique is advisable in all circumstances, but it works here:

def map_aux : Π (i j : fin 4) (hi : to_bool (i.1 < 4 ∧ j.1 < 4 ∧ i ≤ j)), F i ⟶ F j
| ⟨0, _⟩ ⟨0, _⟩ _ := 𝟙 _
| ⟨1, _⟩ ⟨1, _⟩ _ := 𝟙 _
| ⟨2, _⟩ ⟨2, _⟩ _ := 𝟙 _
| ⟨3, _⟩ ⟨3, _⟩ _ := 𝟙 _
| ⟨0, _⟩ ⟨1, _⟩ _ := a
| ⟨1, _⟩ ⟨2, _⟩ _ := b
| ⟨2, _⟩ ⟨3, _⟩ _ := c
| ⟨0, _⟩ ⟨2, _⟩ _ := a ≫ b
| ⟨1, _⟩ ⟨3, _⟩ _ := b ≫ c
| ⟨0, _⟩ ⟨3, _⟩ _ := a ≫ b ≫ c

def map (i j : fin 4) (hij : i ≤ j) : F i ⟶ F j :=
map_aux F a b c i j (to_bool_tt ⟨i.2, j.2, hij⟩)

[Mario Carneiro]

or

def map (i j : fin 4) (hij : i ≤ j) : F i ⟶ F j :=
match i, j, to_bool_tt (⟨i.2, j.2, hij⟩ : i.1 < 4 ∧ j.1 < 4 ∧ i ≤ j) with
| ⟨0, _⟩, ⟨0, _⟩, _ := 𝟙 _
| ⟨1, _⟩, ⟨1, _⟩, _ := 𝟙 _
| ⟨2, _⟩, ⟨2, _⟩, _ := 𝟙 _
| ⟨3, _⟩, ⟨3, _⟩, _ := 𝟙 _
| ⟨0, _⟩, ⟨1, _⟩, _ := a
| ⟨1, _⟩, ⟨2, _⟩, _ := b
| ⟨2, _⟩, ⟨3, _⟩, _ := c
| ⟨0, _⟩, ⟨2, _⟩, _ := a ≫ b
| ⟨1, _⟩, ⟨3, _⟩, _ := b ≫ c
| ⟨0, _⟩, ⟨3, _⟩, _ := a ≫ b ≫ c
end

[Reid Barton]

That's pretty cool, I had no idea about this to_bool method!

[Yaël Dillies]

Oh whoops. I guess I broke it all before fixing it :sweat_smile: