has_coe_to_sort

Stream: new members

[Horatiu Cheval]

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]

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]

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

[Eric Wieser]

Will this will be fixed by Yury's refactor?

[Yury G. Kudryashov]

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.

[Yury G. Kudryashov]

We're talking about lean#557

[Horatiu Cheval]

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]

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]

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