## Stream: general

### Topic: equation compiler help me plz

#### Johan Commelin (Sep 21 2021 at 13:13):

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 (Sep 21 2021 at 13:34):

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 (Sep 21 2021 at 13:36): Not exactly satisfying #### David Wärn (Sep 21 2021 at 13:39): 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 (Sep 21 2021 at 13:44): 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 (Sep 21 2021 at 13:44): 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 (Sep 21 2021 at 13:45): 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 (Sep 21 2021 at 13:51):

Note that this one works:

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


#### David Wärn (Sep 21 2021 at 13:54):

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 (Sep 21 2021 at 13:55):

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 (Sep 21 2021 at 14:12):

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 (Sep 21 2021 at 14:13):

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

#### Yaël Dillies (Sep 21 2021 at 14:19):

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

#### Eric Wieser (Sep 21 2021 at 14:33):

Doesn't it already work for fin n?

#### Yaël Dillies (Sep 21 2021 at 14:40):

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

#### Scott Morrison (Sep 21 2021 at 23:19):

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 (Sep 21 2021 at 23:20):

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 (Sep 21 2021 at 23:23):

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 (Sep 21 2021 at 23:23):

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

#### Scott Morrison (Sep 21 2021 at 23:24):

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

#### Mario Carneiro (Sep 22 2021 at 00:18):

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 (Sep 22 2021 at 00:19):

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 (Sep 22 2021 at 02:29):

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

#### Yaël Dillies (Sep 22 2021 at 06:25):

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

Last updated: Dec 20 2023 at 11:08 UTC