Zulip Chat Archive

Stream: general

Topic: induction with generalize


view this post on Zulip Sarah Mameche (Nov 16 2018 at 22:40):

Hi, I want to do induction over the following predicate types:

inductive types : Π {m}, (fin m  type)  tm m  type  Prop (...)

The predicate expresses Γ ⊢ x : A, where the typing context Γ is a function (fin m→ type) , and expression x has type tm m (but I think the details are not important). My induction is over the empty context:

definition empty_ctx : fin 0  type :=  λ (x : Fin 0), match x with end

Here's the lemma:

lemma preservation (A : type) (e₁ : tm 0) :
  types empty_ctx e₁ A 
      forall e₂, e₁  e₂  types empty_ctx e₂ A :=
begin intros H₁ e H₂,
  induction H₁ (...)

This gives the following error:

[check] application type mismatch at
  types 
argument type
  Fin 0  type
expected type
  Fin _x  type`induction with generalize

In Coq, the induction works. I assume Lean is more strict about generalizing numbers before doing an induction? I'm not sure about how to generalize in this case, as 0 appears in the type of the empty context. So the standard way of adding an assumption h : X = empty_ctx and substituting X doesn't work because X again has type fin 0 → type. Could you give me some details or tell me if I'm on the wrong track?

view this post on Zulip Kenny Lau (Nov 16 2018 at 22:41):

what is Fin?

view this post on Zulip Kenny Lau (Nov 16 2018 at 22:42):

could you provide an MWE?

view this post on Zulip Sarah Mameche (Nov 16 2018 at 22:49):

def Fin : nat  Type
  | 0 := empty
  | (n+1) := option (Fin n)
inductive tm  : nat -> Type
  | var_tm : Π {ntm : nat}, Fin ntm -> tm ntm
  | app : Π {ntm : nat}, tm ntm -> tm ntm -> tm ntm
  | lam : Π {ntm : nat}, tm (nat.succ ntm) -> tm ntm
open tm
inductive type : Type
| tint : type
| tarrow : type  type  type
open type
inductive types : Π {m}, (Fin m  type)  tm m  type  Prop
| tvar {m} Γ (x : Fin m) : types Γ (var_tm x) (Γ x)
| tapp {m} Γ (e₁ : tm m) e₂ (A B) : types Γ e₁ (tarrow A B)  types Γ e₂ A  types Γ (app e₁ e₂) B
--| tlam {m} Γ (e : tm (nat.succ m)) (A B) : types (@scons _ m  A Γ) e B → types Γ (lam e) (tarrow A B) requires some more definitions
definition empty_ctx : Fin 0  type :=  λ (x : Fin 0), match x with end
def step {n} (t t' : tm n) := tt. --(..)
lemma preservation (A : type) (e₁ : tm 0) :
  types empty_ctx e₁ A 
      forall e₂, step e₁  e₂  types empty_ctx e₂ A :=
begin intros H₁ e H₂,
  induction H₁

view this post on Zulip Reid Barton (Nov 16 2018 at 23:03):

I'm not sure how to do it with induction, but I would probably try using the equation compiler

view this post on Zulip Chris Hughes (Nov 16 2018 at 23:04):

Changing the definition of types to this works.

inductive types {m : } : (Fin m  type)  tm m  type  Prop
| tvar Γ (x : Fin m) : types Γ (var_tm x) (Γ x)
| tapp Γ (e₁ : tm m) e₂ (A B) : types Γ e₁ (A  B)  types Γ e₂ A  types Γ (app e₁ e₂) B

view this post on Zulip Reid Barton (Nov 16 2018 at 23:07):

but that won't work for tlam, which increases the size of the context

view this post on Zulip Chris Hughes (Nov 16 2018 at 23:07):

I see.

view this post on Zulip Chris Hughes (Nov 16 2018 at 23:20):

destruct H\1 also works.

view this post on Zulip Chris Hughes (Nov 16 2018 at 23:22):

Although I don't think that gives the goal you want. It didn't choose a very good motive.

view this post on Zulip Chris Hughes (Nov 16 2018 at 23:23):

This is a nasty method that hopefully does get the right goal at least

lemma preservation (A : type) {n} (ctx : Fin n  type) (e₁ : tm 0) :
  types empty_ctx e₁ A 
      forall e₂, step e₁ e₂  types empty_ctx e₂ A :=
λ H₁, @types.rec_on
  (λ m ctx e₁ t, m = 0  ctx == empty_ctx   e₂ : tm m, step e₁ e₂  types ctx e₂ A) 0 empty_ctx e₁ A H₁
    begin
      intros m Γ _ hm hΓ,
      subst hm,
      have := eq_of_heq hΓ,
      subst this,

    end sorry rfl (heq.refl _)

view this post on Zulip Mario Carneiro (Nov 17 2018 at 02:30):

here are a few more options:

lemma preservation (A : type) (e₁ : tm 0)
  (H₁ : types empty_ctx e₁ A) (e₂) (H₂ : step e₁ e₂) : types empty_ctx e₂ A :=
begin
  revert e₁ e₂,
  generalize : empty_ctx = ctx,
  revert ctx,
  generalize h : 0 = n,
  intros,
  induction H₁ generalizing h; subst h,
  { cases H₁_x },
  { sorry }
end

lemma preservation' (A : type) :  (e₁ : tm 0),
  types empty_ctx e₁ A   e₂, step e₁ e₂  types empty_ctx e₂ A :=
suffices  {n}, n = 0   {ctx} (e₁ : tm n), types ctx e₁ A   e₂, step e₁ e₂  types ctx e₂ A,
from this rfl,
begin
  introv h H₁ H₂,
  induction H₁ generalizing h; subst h,
  { cases H₁_x },
  { sorry }
end

view this post on Zulip Mario Carneiro (Nov 17 2018 at 02:31):

in this case it doesn't matter that you have empty_ctx since it's unique anyway

view this post on Zulip Sarah Mameche (Nov 17 2018 at 07:59):

Great, thanks!


Last updated: May 14 2021 at 04:22 UTC