Zulip Chat Archive

Stream: new members

Topic: Sizeof for types in Prop


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

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

view this post on Zulip Mario Carneiro (Mar 22 2020 at 15:19):

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

view this post on Zulip Mario Carneiro (Mar 22 2020 at 15:21):

do you have an example?

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

view this post on Zulip Anton Lorenzen (Mar 22 2020 at 15:23):

More specifically the using_well_founded part

view this post on Zulip Anton Lorenzen (Mar 22 2020 at 15:26):

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

view this post on Zulip Mario Carneiro (Mar 22 2020 at 15:27):

Use tactic mode and induction to prove it, instead of using the equation compiler

view this post on Zulip Mario Carneiro (Mar 22 2020 at 15:28):

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

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

view this post on Zulip Anton Lorenzen (Mar 22 2020 at 15:30):

What is this usual order?

view this post on Zulip Mario Carneiro (Mar 22 2020 at 15:31):

Structural recursion

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

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

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

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

view this post on Zulip Mario Carneiro (Mar 22 2020 at 15:35):

that's what the generalize line is for

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

view this post on Zulip Anton Lorenzen (Mar 22 2020 at 15:36):

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

view this post on Zulip Anton Lorenzen (Mar 22 2020 at 15:36):

Same with b but not with a or e

view this post on Zulip Mario Carneiro (Mar 22 2020 at 15:37):

show me your code?

view this post on Zulip Anton Lorenzen (Mar 22 2020 at 15:37):

Using only generalize a e followed by cases e doesnt help

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

view this post on Zulip Anton Lorenzen (Mar 22 2020 at 15:37):

Or all of it?

view this post on Zulip Mario Carneiro (Mar 22 2020 at 15:38):

the generalize line fails?

view this post on Zulip Mario Carneiro (Mar 22 2020 at 15:38):

Oh, you have to intro h after the generalize

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

view this post on Zulip Mario Carneiro (Mar 22 2020 at 15:39):

semicolon before cases

view this post on Zulip Anton Lorenzen (Mar 22 2020 at 15:40):

Oh, that does the trick!

view this post on Zulip Anton Lorenzen (Mar 22 2020 at 15:40):

Where can I read more about that black magic?

view this post on Zulip Mario Carneiro (Mar 22 2020 at 15:40):

which part?

view this post on Zulip Mario Carneiro (Mar 22 2020 at 15:41):

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

view this post on Zulip Anton Lorenzen (Mar 22 2020 at 15:41):

Ah okay!

view this post on Zulip Anton Lorenzen (Mar 22 2020 at 15:42):

Let's see if I can prove it now

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

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

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