Sizeof for types in Prop

Stream: new members

[Anton Lorenzen]

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]

there is no way to define a sizeof for Prop valued inductive predicates, unless they are large eliminating

[Mario Carneiro]

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

[Mario Carneiro]

do you have an example?

[Anton Lorenzen]

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]

More specifically the using_well_founded part

[Anton Lorenzen]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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]

What is this usual order?

[Mario Carneiro]

Structural recursion

[Anton Lorenzen]

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

I still don't understand that

[Mario Carneiro]

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]

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

[Anton Lorenzen]

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]

that's what the generalize line is for

[Mario Carneiro]

You can follow up the induction line with ; cases e and it should clear those cases up

[Anton Lorenzen]

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

[Anton Lorenzen]

Same with b but not with a or e

[Mario Carneiro]

show me your code?

[Anton Lorenzen]

Using only generalize a e followed by cases e doesnt help

[Anton Lorenzen]

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]

Or all of it?

[Mario Carneiro]

the generalize line fails?

[Mario Carneiro]

Oh, you have to intro h after the generalize

[Anton Lorenzen]

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]

semicolon before cases

[Anton Lorenzen]

Oh, that does the trick!

[Anton Lorenzen]

Where can I read more about that black magic?

[Mario Carneiro]

which part?

[Mario Carneiro]

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

[Anton Lorenzen]

Ah okay!

[Anton Lorenzen]

Let's see if I can prove it now

[Mario Carneiro]

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]

You can also do tac1; [tac2, tac2, tac2, tac2, tac2] to apply tac2 on all the goals created by tac1

[Anton Lorenzen]

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