Zulip Chat Archive

Stream: general

Topic: equation compiler

Minchao Wu (Jul 24 2018 at 16:56):

Hi friends, is there a way to fill up this underscore?

def foo (n : nat) : nat :=
match n with
| 0     := 0
| k     := have k ≠ 0, from _,
           0
end

Usually n is of some complicated inductive types, but I really just need to handle one specific constructor. For all the other constructors the proofs are long but exactly the same.
I could use rec or cases or if then else but that would be awkward. So I am wondering how I can refer to the facts that the equation compiler knows but are not listed as hypotheses?

Kenny Lau (Jul 24 2018 at 16:56):

use k+1 instead of k

Minchao Wu (Jul 24 2018 at 16:57):

that works in the case of nat but not other complicated inductive types

Kenny Lau (Jul 24 2018 at 16:57):

then you can't

Minchao Wu (Jul 24 2018 at 16:59):

def bar : bool → ℕ
| tt     := 0
| b     := have b ≠ tt, from _, 1

well maybe this one is a better toy example

Kenny Lau (Jul 24 2018 at 17:00):

you can't.

Minchao Wu (Jul 24 2018 at 17:00):

reason?

Kenny Lau (Jul 24 2018 at 17:00):

in that environment you do not know that b is not tt

Kenny Lau (Jul 24 2018 at 17:01):

also how do you use rec or cases?

Minchao Wu (Jul 24 2018 at 17:01):

but the equation compiler knows that if it's tt then the thing is not exhaustive

Kenny Lau (Jul 24 2018 at 17:01):

the b is a catch-all clause

Kenny Lau (Jul 24 2018 at 17:01):

it is intended to match everything

Minchao Wu (Jul 24 2018 at 17:01):

that's true

Minchao Wu (Jul 24 2018 at 17:02):

I am saying that the compiler knows that tt will never be matched by b

Kenny Lau (Jul 24 2018 at 17:02):

but that's already outside your environment

Minchao Wu (Jul 24 2018 at 17:03):

perhaps, so I am asking if there is a clever hack

Kenny Lau (Jul 24 2018 at 17:03):

what was your idea with rec and cases?

Minchao Wu (Jul 24 2018 at 17:04):

also how do you use rec or cases?

you just don't use match

Kenny Lau (Jul 24 2018 at 17:04):

that works in the case of nat but not other complicated inductive types

does using rec solve this problem?

Minchao Wu (Jul 24 2018 at 17:05):

it's the same as your suggestion of using (k+1)

Minchao Wu (Jul 24 2018 at 17:05):

namely explicitly writing down all the constructors

Simon Hudon (Jul 24 2018 at 17:28):

What you could do is:

begin
  cases n,
  case 0 :
  { /- proof -/ },
  all_goals { /- proof -/ },
end

Kenny Lau (Jul 24 2018 at 17:28):

but how are you going to prove n != 0?

Johan Commelin (Jul 24 2018 at 17:31):

I think that you don't have to.

Johan Commelin (Jul 24 2018 at 17:31):

That is Simon's trick.

Johan Commelin (Jul 24 2018 at 17:32):

You just prove it case by case, for all cases. But then, you prove all but one case with a single proof.

Minchao Wu (Jul 24 2018 at 17:33):

I forgot to mention that foll all the other cases I need the fact that n!=0

Minchao Wu (Jul 24 2018 at 17:34):

but this trick might work

Johan Commelin (Jul 24 2018 at 17:35):

Right, so now you somehow need to know that fact, but now it should be even true in your environment (I hope).

Simon Hudon (Jul 24 2018 at 17:35):

Off the top of my head, cases h : n will preserve the variable n and you can do your proof with subst n and contradiction

Simon Hudon (Jul 24 2018 at 17:44):

concretely, here is how I do it:

def foo (n : nat) : nat :=
begin
  cases h : n,
  case nat.zero :
  { exact 0 },
  all_goals
  { have : n ≠ 0,
    { subst n, contradiction },
    exact n },
end