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

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


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!

which part?

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

tac1; tac2 does tac1, and then does tac2 on every subgoal created by tac1

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