term mode partial function correctness proof?

Stream: new members

[Johannes C. Mayer]

I am trying to do the exercise at the end of 7.2 in theorem proving in LEAN. I am a bit confused. How can you prove the second example in term mode?

namespace hidden
universe u

variables {α β γ : Type*}

inductive option (α : Type u) : Type u
| none : option
| some : α → option

def comp_partial (f : α → option β) (g : β → option γ) : α → option γ :=
λ ha, option.cases_on (f ha) option.none (λ hb, g hb)

variables (f : α → option β)
          (g : β → option γ)

example (x : α) (h₁ : f x = option.none) :
  ((comp_partial f g) x) = option.none :=
begin
  unfold comp_partial,
  rewrite h₁,
end

-- How to do this in term mode?
example (x : α) (h₁ : f x = option.none) :
  ((comp_partial f g) x) = option.none :=
sorry

end hidden

[Mario Carneiro]

the short answer is that you shouldn't, tactic mode does this one better

[Mario Carneiro]

The long answer is

example (x : α) (h₁ : f x = option.none) : ((comp_partial f g) x) = option.none :=
@congr_arg _ (option γ) _ _ (λ y, option.cases_on y option.none g) h₁

[Patrick Johnson]

Use show_term to see what the tactics compiled into:

begin
  show_term {
    unfold comp_partial,
    rewrite h₁}
end

[Johannes C. Mayer]

@Patrick Johnson That does give me something, but it is extremely complicated, or at least pretty long. Right now I also don't get Mario's answer but that seems much easier to understand.

[Mario Carneiro]

The hard part in the proof is rw, which makes for messy term proofs. I will usually use rw even in a term mode proof because it's more reliable and about as fast

[Mario Carneiro]

The basic idea is that if you have some goal P x containing a subterm x and you want to replace it with y given an equation h : x = y, then use congr_arg P h which has the type P x = P y

[Mario Carneiro]

the hard part is that you have to write down P, where rw will figure it out automatically by finding all instances of x in the goal and replacing them with a lambda variable

[Mario Carneiro]

the other hard part in this particular problem is that option.cases_on has a dependent type and this gives the elaborator trouble once it is removed from the context of comp_partial where the type is known. This is why I had to specify the type option γ to congr_arg

[Mario Carneiro]

The term used by rw involves eq.rec, which is very difficult to write manually unless you specify a bunch of implicit arguments because it has some unusual elaboration rules

[Johannes C. Mayer]

It also seems like even show_term can't handle eq.rec. I get: "invalid 'eq.rec' application, elaborator has special support for this kind of application (it is handled as an "eliminator"), but expected type must not contain metavariables", when I simply click on the 'try this' of show_term.

[Mario Carneiro]

that's what I mean

[Mario Carneiro]

the lean 3 pretty printer has trouble round-tripping at the default printing settings when eq.rec is involved

[Mario Carneiro]

you have to set_option pp.all true or so, which will also make the output rather hard to read

[Johannes C. Mayer]

YES, that works. And also it makes the proof just hilariously long :joy: . 101 lines in fact.

[Johannes C. Mayer]

@Mario Carneiro I do get your proof now I think. It creates the term option.cases_on (f x) option.none g = option.none right? And then LEAN looks at this and notices that it is definitionally equal to comp_partial f g x = option.none.

Is there some way to make this last step more explicit? E.g. could we specify a rewrite operation to rewrite option.cases_on (f x) option.none g to comp_partial f g x?