# Zulip Chat Archive

## Stream: new members

### Topic: Sizeof for types in Prop

#### Anton Lorenzen (Mar 22 2020 at 15:17):

I am currently refactoring a type to be in Prop instead of Type and this is breaking the well-foundedness proof of a function since the `mytype.sizeof`

function doesn't exist anymore. Is there an easy way to fix this? And why is there no `sizeof`

for types in Prop (that only eliminates into Prop or so..)?

#### Mario Carneiro (Mar 22 2020 at 15:18):

there is no way to define a `sizeof`

for Prop valued inductive predicates, unless they are large eliminating

#### Mario Carneiro (Mar 22 2020 at 15:19):

or if they have some other special property specific to the set up

#### Mario Carneiro (Mar 22 2020 at 15:21):

do you have an example?

#### Anton Lorenzen (Mar 22 2020 at 15:23):

From the type checker I sent you. I figured out how to put Judgement into Prop, but now this lemma is breaking:

lemma typing_pi : Π {g x a b t}, Judgement g (Exp.pi x a b) t → ∃ s, Judgement g a (Exp.sort s) | g x a b t (@Judgement.product _ _ _ _ s _ _ r ta _) := ⟨s, ta⟩ | g x a b t (@Judgement.conv _ _ _ _ _ _ _ tr) := typing_pi tr | (Context.cons _ _ _) x a b t (@Judgement.weaken _ _ _ _ s _ h j js) := let ⟨res, j2⟩ := typing_pi j in ⟨res, @Judgement.weaken _ _ _ _ s _ h j2 js⟩ using_well_founded { rel_tac := λ _ _, `[exact ⟨_, measure_wf (λ j, begin rcases j with ⟨g, x, a, b, t, j⟩, exact Judgement.sizeof g (Exp.pi x a b) t j, end)⟩ ] }

#### Anton Lorenzen (Mar 22 2020 at 15:23):

More specifically the `using_well_founded`

part

#### Anton Lorenzen (Mar 22 2020 at 15:26):

I can push the whole code to Github in half an hour or so

#### Mario Carneiro (Mar 22 2020 at 15:27):

Use tactic mode and `induction`

to prove it, instead of using the equation compiler

#### Mario Carneiro (Mar 22 2020 at 15:28):

is that well founded metric different from the usual structural order on `Judgment`

?

#### Mario Carneiro (Mar 22 2020 at 15:30):

can't typecheck so I might have the details wrong, but the setup should look something like this:

lemma typing_pi {g x a b t} (h : Judgement g (Exp.pi x a b) t) : ∃ s, Judgement g a (Exp.sort s) := begin generalize e : Exp.pi x a b = y, induction h generalizing x a b e, end

#### Anton Lorenzen (Mar 22 2020 at 15:30):

What is this usual order?

#### Mario Carneiro (Mar 22 2020 at 15:31):

Structural recursion

#### Anton Lorenzen (Mar 22 2020 at 15:32):

is that well founded metric different from the usual structural order on Judgment?

I still don't understand that

#### Mario Carneiro (Mar 22 2020 at 15:33):

I shouldn't actually call it an order since we're talking about props here, it's an order on the terms at the metalevel

#### Mario Carneiro (Mar 22 2020 at 15:34):

basically the arguments to a constructor are less than the conclusion, and the structural order is the minimal order satisfying that property

#### Anton Lorenzen (Mar 22 2020 at 15:35):

The problem with the induction tactic is that it doesn't recognize that not all constructors can give that type and makes me prove the lemma for all of them.

#### Mario Carneiro (Mar 22 2020 at 15:35):

that's what the `generalize`

line is for

#### Mario Carneiro (Mar 22 2020 at 15:36):

You can follow up the `induction`

line with `; cases e`

and it should clear those cases up

#### Anton Lorenzen (Mar 22 2020 at 15:36):

The second generalize says get_local tactic failed, unknown 'x' local

#### Anton Lorenzen (Mar 22 2020 at 15:36):

Same with b but not with a or e

#### Mario Carneiro (Mar 22 2020 at 15:37):

show me your code?

#### Anton Lorenzen (Mar 22 2020 at 15:37):

Using only `generalize a e`

followed by `cases e`

doesnt help

#### Anton Lorenzen (Mar 22 2020 at 15:37):

lemma typing_pi : Π {g x a b t}, Judgement g (Exp.pi x a b) t → ∃ s, Judgement g a (Exp.sort s) := begin intros g x a b t h, generalize e : Exp.pi x a b = y, induction h generalizing a e, cases e, end

#### Anton Lorenzen (Mar 22 2020 at 15:37):

Or all of it?

#### Mario Carneiro (Mar 22 2020 at 15:38):

the `generalize`

line fails?

#### Mario Carneiro (Mar 22 2020 at 15:38):

Oh, you have to intro `h`

after the `generalize`

#### Anton Lorenzen (Mar 22 2020 at 15:39):

Better, no get_local error. But still too many cases

lemma typing_pi : Π {g x a b t}, Judgement g (Exp.pi x a b) t → ∃ s, Judgement g a (Exp.sort s) := begin intros g x a b t, generalize e : Exp.pi x a b = y, intro h, induction h generalizing x a b e, cases e, end

#### Mario Carneiro (Mar 22 2020 at 15:39):

semicolon before `cases`

#### Anton Lorenzen (Mar 22 2020 at 15:40):

Oh, that does the trick!

#### Anton Lorenzen (Mar 22 2020 at 15:40):

Where can I read more about that black magic?

#### Mario Carneiro (Mar 22 2020 at 15:40):

which part?

#### Mario Carneiro (Mar 22 2020 at 15:41):

`tac1; tac2`

does `tac1`

, and then does `tac2`

on every subgoal created by `tac1`

#### Anton Lorenzen (Mar 22 2020 at 15:41):

Ah okay!

#### Anton Lorenzen (Mar 22 2020 at 15:42):

Let's see if I can prove it now

#### Mario Carneiro (Mar 22 2020 at 15:42):

`tac1, tac2`

by contrast applies `tac2`

in the context of all the goals created by `tac1`

, which for most tactics means that it will only do something to the first goal created by `tac1`

#### Mario Carneiro (Mar 22 2020 at 15:43):

You can also do `tac1; [tac2, tac2, tac2, tac2, tac2]`

to apply `tac2`

on all the goals created by `tac1`

#### Anton Lorenzen (Mar 22 2020 at 15:56):

Alright:

lemma typing_pi : Π {g x a b t}, Judgement g (Exp.pi x a b) t → ∃ s, Judgement g a (Exp.sort s) := begin intros g x a b t, generalize e : Exp.pi x a b = y, intro h, induction h generalizing e; cases e, { cases h_ih_a (eq.refl _), apply exists.intro w, apply Judgement.weaken, exact h_noShadowing, exact h, exact h_a_1, }, { exact ⟨h_s1, h_a⟩ }, { from h_ih_a_1 (eq.refl _) }, end

Though I have to say that I found the old version a lot more readable..

Last updated: May 11 2021 at 22:14 UTC