# Zulip Chat Archive

## 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