# Zulip Chat Archive

## Stream: general

### Topic: induction with generalize

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

#### Kenny Lau (Nov 16 2018 at 22:41):

what is `Fin`

?

#### Kenny Lau (Nov 16 2018 at 22:42):

could you provide an MWE?

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

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

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

#### Reid Barton (Nov 16 2018 at 23:07):

but that won't work for `tlam`

, which increases the size of the context

#### Chris Hughes (Nov 16 2018 at 23:07):

I see.

#### Chris Hughes (Nov 16 2018 at 23:20):

`destruct H\1`

also works.

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

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

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

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

#### Sarah Mameche (Nov 17 2018 at 07:59):

Great, thanks!

Last updated: May 14 2021 at 04:22 UTC