## Stream: new members

### Topic: has_coe_to_sort

#### Horatiu Cheval (Mar 28 2021 at 07:55):

I think I am misunderstanding has_coe_to_sort. Why does the following not work?

inductive formula {α : Type} [has_coe_to_sort α]
| equation {a : α} : a → a → formula
--type expected at
--  a
--term has type
--  α


#### Mario Carneiro (Mar 28 2021 at 08:09):

I don't think has_coe_to_sort works as an assumption, because it is necessary for the first projection out of the has_coe_to_sort instance to definitionally reduce to Sort u, which isn't possible unless you have a concrete instance

#### Horatiu Cheval (Mar 28 2021 at 08:12):

Oh, ok. It worked indeed with concrete choices of α, and that amplified my confusion. Thanks!

#### Eric Wieser (Mar 28 2021 at 08:53):

Will this will be fixed by Yury's refactor?

#### Yury G. Kudryashov (Mar 28 2021 at 14:29):

I wouldn't call it "Yury's" refactor. It is backporting of coe_sort and coe_fun from Lean 4, and most of the hard work in core was done by @Gabriel Ebner.

#### Horatiu Cheval (Mar 28 2021 at 21:24):

Another problem I encountered in the same context which might be related (though, I am not sure if it's due to has_coe_to_sort).
Why is the inductive definition of proof wrong, why are there several σ's generated?

inductive linear_type
| zero : linear_type
| arrow : linear_type → linear_type → linear_type

infixr ↣ : 50 := linear_type.arrow
notation 𝕋 := linear_type

instance : has_zero 𝕋 := ⟨linear_type.zero⟩

def linear_type_to_sort : 𝕋 → Type
| 0 := ℕ
| (σ ↣ τ) := (linear_type_to_sort σ) → (linear_type_to_sort τ)

instance : has_coe_to_sort linear_type := ⟨Type, linear_type_to_sort⟩

inductive formula
| equation : (0 : 𝕋) → (0 : 𝕋) → formula
| universal : ∀ (σ : 𝕋) (A : σ → formula), formula

notation ∀' := formula.universal

def equation_ext : ∀ {σ : 𝕋}, σ → σ → formula
| 0 := λ t u, formula.equation t u
| (σ ↣ τ) := λ t u : (σ ↣ τ), ∀' σ (λ x : σ, equation_ext (t x) (u x))

inductive proof (Γ : list formula) : formula → Type
| EXT : ∀ {σ τ : 𝕋} {t u : σ} {s : (σ ↣ τ)},
proof (@equation_ext σ t u) → proof (@equation_ext τ (s t) (s u))

/-
type mismatch at application
equation_ext t
term
t
has type
↥σ_1
but is expected to have type
↥σ
types contain aliased name(s): σ
remark: the tactic dedup can be used to rename aliases
-/


#### Mario Carneiro (Mar 28 2021 at 22:51):

This looks like a bug, although I'm not sure where. As a workaround, this works:

inductive proof (Γ : list formula) : formula → Type
| EXT : ∀ {σ τ : 𝕋} {t u : σ} {s : (σ ↣ τ)} {f},
f = (@equation_ext τ (s t) (s u)) →
proof (@equation_ext σ t u) → proof f


#### Mario Carneiro (Mar 28 2021 at 22:56):

This also works:

inductive proof (Γ : list formula) : formula → Type
| EXT : ∀ {σ τ : 𝕋} {t u : σ} {s : (σ ↣ τ)},
proof (@equation_ext σ t u) → proof (@equation_ext τ (id s t) (s u))


Last updated: May 09 2021 at 19:11 UTC