Zulip Chat Archive

Stream: new members

Topic: has_coe_to_sort


view this post on Zulip 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
--  α

view this post on Zulip 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

view this post on Zulip Horatiu Cheval (Mar 28 2021 at 08:12):

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

view this post on Zulip Eric Wieser (Mar 28 2021 at 08:53):

Will this will be fixed by Yury's refactor?

view this post on Zulip 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.

view this post on Zulip Yury G. Kudryashov (Mar 28 2021 at 14:30):

We're talking about lean#557

view this post on Zulip 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
-/

view this post on Zulip 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

view this post on Zulip 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