Help with Inductively Defined Propositions

Stream: new members

[Jonathan Bryant]

Hey, everybody! I'm Jonathan. Nice to meet y'all.

I'm new to Theorem Proving/Formal Methods and I'm actually really enjoying it. I've been teaching myself from a few resources I found online, but primarily Theorem Proving in Lean and the Software Foundation series. I've been doing SF in Lean because I like the language better than Coq.

I was doing well with it until I got to inductively defined propositions. I'm fundamentally not quite grokking something about them. I get how they're supposed to work from my experience with Types and Programming Languages (I'm a compiler geek), but I'm struggling to actually manipulate the values in Lean to construct proofs. Unfortunately, I don't quite understand what I don't understand so I haven't been able to ask a coherent question about it.

But I think I finally found an illustrative example. I've put it up in a Gist with a lot of comments and some specific questions. If I could get some feedback/help with it I would appreciate it.

Thanks!

[Kevin Buzzard]

I think one of your questions is "what is the lean analogue of the Coq inversion tactic?" and I've heard before that the answer is cases.

[Kevin Buzzard]

See for example https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Behaviour.20of.20.60cases.60.20depends.20on.20type.20constructor.20args'.20order

[A.]

(deleted)

[A.]

Apologies, these responses purely in code probably weren't very helpful. I have deleted them and hopefully someone who knows something about the internals of Lean will come up with real explanations.

[Jonathan Bryant]

Well, asking the question made it clearer for me. After sleeping on it, for the term-style it was a one-liner:

have mp: CommandEval (Command.seq .skip c) s₁ s₂ → CommandEval c s₁ s₂
  | .seq .skip c _ _ s₃ (.skip s) h₂ => h₂

I realized that I didn't need to show the equivalence explicitly. By matching _ for s1 and s2 while on (.skip s) for h1, it implicitly figured out the equality for me. Once I figured that out, for the tactic style I immediately came up with exactly what @Alistair Tucker suggested and it worked.

I've found other cases where I fiddled with it long enough and came across similar solutions. It's another case of once I saw it it made sense, but I couldn't actively reason towards the solution. Maybe what I don't understand is dependent pattern matching? Any deeper dive resources on that?

[Jonathan Bryant]

Kevin Buzzard said:

I think one of your questions is "what is the lean analogue of the Coq inversion tactic?" and I've heard before that the answer is cases.

Maybe? cases seems to be roughly analogous to destruct from Coq, though admittedly it may be doing more behind the scenes than I realize. There's several places where there's not 1:1 mappings between tactics so could be the case. So far, I've been viewing cases as just that: a straightforward case or match construct. Is there some hidden depth I'm missing?

[Jonathan Bryant]

Another reason I think my underlying gap might be dependent pattern matching is that I never would have expected the h2 in the nested cases to come up with the right set of state variables, so I never would have thought to use it to get the solve. And I still don't understand how or why it did that.

[Jonathan Bryant]

Alistair Tucker said:

Apologies, these responses purely in code probably weren't very helpful. I have deleted them and hopefully someone who knows something about the internals of Lean will help you with real explanations.

No, no, no. Code is wonderful. I speak code way more fluently than I speak math or meta-theory.

[Jonathan Bryant]

Maybe I can ask a more concrete question. I understand "normal" pattern matching (for example, this paper by Maranget on compiling pattern matching to decision trees). Is there something that can extend that understanding to dependent pattern matching so that I can understand what's different and how it's resolving those cross-pattern dependencies?

[Kevin Buzzard]

Jonathan Bryant said:

Alistair Tucker said:

Apologies, these responses purely in code probably weren't very helpful. I have deleted them and hopefully someone who knows something about the internals of Lean will help you with real explanations.

No, no, no. Code is wonderful. I speak code way more fluently than I speak math or meta-theory.

Note that you can still see the code if you're on a computer -- just click the word "EDITED" by Alistair's name to see the edit history. Note @Alistair Tucker this is one of several reasons why it's a bit silly to delete your helpful code.

[A.]

I thought to leave them there might give the impression that I was "on the case".

[Jonathan Bryant]

Unification. That's what I was missing. Specifically, Higher-Order Unification.

Once I figured that out, I made tons of progress. It also answered a bunch of other queestions I had that I couldn't even articulate. So I'll take the time to answer my own question here in the hope that if anyone searches and stumbles across this thread, it will help.

In the original example, I was asking why I couldn't compute the "obviously" true sorry below:

inductive Command: Type where
  | skip: Command
  -- ... Other constructors ...

inductive CommandEval: Command → State → State → Prop where
  | skip (s: State): CommandEval .skip s s
  | assign {e: Arith} {n: Nat} {id: String} (s: State) (h: e.eval s = n): CommandEval (.assign id e) s (s.update id n)
  | seq {c₁ c₂: Command} (s₁ s₂ s₃: State) (h₁: CommandEval c₁ s₁ s₂) (h₂: CommandEval c₂ s₂ s₃): CommandEval (.seq c₁ c₂) s₁ s₃
  | ifTrue {c: Logic} {t f: Command} (s₁ s₂: State) (h₁: c.eval s₁ = .true) (h₂: CommandEval t s₁ s₂): CommandEval (.if c t f) s₁ s₂
  | ifFalse {c: Logic} {t f: Command} (s₁ s₂: State) (h₁: c.eval s₁ = .false) (h₂: CommandEval f s₁ s₂): CommandEval (.if c t f) s₁ s₂
  | whileTrue {c: Logic} {b: Command} (s₁ s₂ s₃: State) (h₁: c.eval s₁ = .true) (h₂: CommandEval b s₁ s₂) (h₃: CommandEval (.while c b) s₂ s₃): CommandEval (.while c b) s₁ s₃
  | whileFalse {c: Logic} {b: Command} (s: State) (h₁: c.eval s = .false): CommandEval (.while c b) s s

example: CommandEval (Command.seq .skip c) s₁ s₂ → CommandEval c s₁ s₂
  | .seq s₁ s₂ s₃ h₁ h₂ =>
    have h₃: s₁ = s₂ :=
      sorry
    by
      rw [← h₃] at h₂
      exact h₂

But the following much simpler code did work, as if by magic:

example: CommandEval (Command.seq .skip c) s₁ s₂ → CommandEval c s₁ s₂
  | .seq _ _ _ (.skip _) h₂ => h₂

That "magic" is Unification. I'm used to thinking of unification as something that happens at the type level, as in Hindley-Milner inference. But since Lean is dependently typed, types and terms are interchangeable. So Lean is performing (higher-order) unification over not just the type the entire expression: types, terms, everything.

What's happening is that when I leave the states (the s₁, s₂, and s₃) as holes (_) for the unifier to figure out and explicitly write out that the first hypothesis h₁ is the term (.skip _), itself with a hole, the unifier automatically deduces that since the type of the .skip _ is CommandEval .skip s s, the holes for s₁ and s₂ as well as the hole for the state of the .skip must all be equal, which is exactly what I was trying to prove explicitly.

This understanding that unification is happening everywhere also answered several other questions:

• Why don't I have to explicitly list all combinatorial patterns, but also not have to put wildcard _ patterns? Because unification is being performed. Any pattern that can't possibly unify with the result is automatically excluded.
• What's the Lean equivalent of the inversion tactic and why is it cases? Because unification. Just like matching, the cases tactic (as well as the induction tactic) performs unification and excludes any cases that can't possibly unify. This is precisely what Coq's inversion tactic is doing: using evidence to exclude unreachable possibilities.
• Why did I have to explicitly handle my ifTrue/ifFalse and whileTrue/whileFalse cases? You guessed it: unification! When the type of the proposition is CommandEval (.if ...) ..., either of the ifTrue and ifFalse rules could unify with it, so both have to be handled, even if one is immediately contradictory. Similar for the CommandEval (.while ...) ... types.
• Why, if the apply tactic is interactive function application, do I only have to give some of the arguments, not all? How come which ones I specify seems to change as I work through the proof? Because you only have to supply the arguments the unifier can't come up with on its own. If you give an argument (with exact or assumption or trivial or some other tactic) that happens to be dependent type, it helps the unifier unify away more arguments from the environment and it can shorten the list of arguments you need to provide.
• How do implicit arguments work? How do I know what can be implicit? Implicit arguments are arguments that you are specifically saying the unifier should be able to work out on its own from the context. Specifically, they should be arguments that are dependended on by later types, since there are no other values that those arguments could possibly be. In the above type, all the Command values (as well as Nat, String, Logic, and Arith) values are implicit because they're mentioned in the non-implicit hypotheses arguments. All of the State arguments could also be made implicit since they're mentioned in those non-implicit arguments as well. (They were left explicit here for the purposes of illustrating the answer to the question.)

This makes Lean's already impressive pattern matching facilities just that much more powerful. In Lean, you can match on any inductive type. And since it's the Calculus of Inductive Constructions, everything is an inductive type (which TPiL does a good job of pointing out.) So now I'm letting my guiding mantra be "Match. All. The. Things." and it's working a lot better.

Thanks @Alistair Tucker and @Kevin Buzzard for your initial help.

[Jonathan Bryant]

But now I have a new question. I'm trying to prove transitivity of certain relations, specifically the Transitive and the Reflexive Transitive closure of other Relations.

I can do the proof using tactics (section ProveTheSorry), but when I try to create the induction hypothesis manually using a recursive call, it complains that I didn't prove termination and my call is not structural induction. I'm doing a nearly identical thing here (and other places), so I know the basic technique works. And the h_y is a sub-term, so it would intuitively seem that this call would work.

Any hints as to why Lean doesn't like this?

def Relation (α: Type): Type := α → α → Prop

inductive TClos (R: Relation α): Relation α
  | base {x y: α} (hxy: R x y): TClos R x y
  | step {x y z: α} (hxy: R x y) (hyz: TClos R y z): TClos R x z

inductive RTClos (R: Relation α): Relation α :=
  | refl {x: α}: RTClos R x x
  | step {x y z: α} (hxy: R x y) (hyz: RTClos R y z): RTClos R x z

theorem TClos.transitive {R: Relation α} {x y z: α}: TClos R x y → TClos R y z → TClos R x z
  | .base h, hyz => .step h hyz
  | .step hx_ h_y, hyz =>
    have ih: TClos R _ z → TClos R _ z := sorry
      -- Why does this fail to be structurally inductive?
      -- | hyz => TClos.transitive h_y hyz
    .step hx_ (ih hyz)

theorem RTClos.transitive {R: Relation α} {x y z: α}: RTClos R x y → RTClos R y z → RTClos R x z
  | .refl, hyz => hyz
  | .step hx_ h_y, hyz =>
    have ih: RTClos R _ z → RTClos R _ z := sorry
      -- Why does this fail to be structurally inductive?
      -- | hyz => RTClos.transitive h_y hyz
    .step hx_ (ih hyz)

section ProveTheSorry
  example {R: Relation α} {x y z: α} (hxy: TClos R x y) (hyz: TClos R y z): TClos R x z := by
    induction hxy with
      | base h =>
        apply TClos.step
        · exact h
        · exact hyz
      | step hx_ h_y ih =>
        apply TClos.step
        · exact hx_
        · apply ih
          · exact hyz

  example {R: Relation α} {x y z: α} (hxy: RTClos R x y) (hyz: RTClos R y z): RTClos R x z := by
    induction hxy with
      | refl => exact hyz
      | step hx_ h_y ih =>
        apply RTClos.step
        · exact hx_
        · apply ih
          · exact hyz
end ProveTheSorry

[Mario Carneiro]

This is because lean's equation compiler does not handle inductive propositions very well, it uses a compilation strategy that was designed for recursive functions and doesn't work in the inductive proposition case. induction is the workaround

[Mario Carneiro]

Note that lean's equation compiler does not actually support structural induction, it uses "bounded induction" instead using the T.brecOn function which is automatically defined, but this definition fails for prop inductives

[Mario Carneiro]

in fact this example looks almost identical to the one in lean4#1672

[Jonathan Bryant]

:smiling_face_with_tear: How unfortunate.

[Preeyan Parmar]

I'm extremely new to Lean (but have a good mathematical and programming background).

I'm finding this example instructive to learn from. I have a couple of questions, some very basic. I've simplified the example to

def Relation (α: Type): Type := α → α → Prop

inductive TClos (R: Relation α) : Relation α
  | base {x y: α} (hxy: R x y) : TClos R x y
  | step {x y z: α} (hxy: R x y) (hyz: TClos R y z) : TClos R x z

def right_hand_step {R: Relation α} {x y z: α} : TClos R x y → R y z → TClos R x z
  | .base hxy, hyz => .step hxy (.base hyz)
  | .step hxw hwy, hyz => .step hxw (right_hand_step hwy hyz)

1. What's the difference between theorem and def? (I scanned the docs, but didn't find anything. Searching for "theorem" is quite noisy...)

2. Is there an explanation of the member access . in .base? (I understand that it is inferring TClos on the left somehow, but is there an explanation of precisely what can be inferred this way?)

3. You can see that I want hxw in the last line to have type R x w but it actually has type R x y✝ when I hover over it. Is there a way to do this? I tried replacing hxw with (hxw : R x w) but then I got an error about w being unknown. Adding w to the implicit argument list seems undesirable (because this is 'internal' to the definition) and in any case then causes an error in the second-last line because w can't be inferred in that line.

4. Your answer "induction is the workaround" - is this what you mean? (Lean tells me it's correct, but is it what you meant?)

def right_hand_step {R: Relation α} {x y z : α} (hxy : TClos R x y) (hyz : R y z) : TClos R x z :=
  by induction hxy with
  | base hxy => exact .step hxy (.base hyz)
  | step hxw _ ih => exact .step hxw (ih hyz)

5. Is it possible to write this definition without tactics? (My rudimentary understanding of type theory suggests that there might be a term called an 'induction principle' or 'dependent eliminator' that I could use?)

Apologies if any of this is in the various tutorials - I have had a quick look already.

[Edward van de Meent]

i'm relatively new too, so it might not be entirely accurate, but i think one of the differences between def and theorem is that with def, lean "remembers" the content of the definition, while with theorem, it doesn't.

a simple example:

import Init.Prelude
open Nat
def foo : Nat := 1
example: foo = 1 := rfl -- works

theorem bar : Nat := 1

example: bar = 1 := rfl -- doesn't work

[Edward van de Meent]

from a mathematical standpoint, it makes sense to have such "forgetful" definitions, because often you don't care a lot about in what way you have proven a statement (read: created an object of a type), but just that there is one. also, (i'm guessing) some proofs of statements get very large, to the point that it isn't efficient to store the exact proof either.

[Kevin Buzzard]

Somehow there's no point storing a proof, because in Lean any two proofs of a proposition are equal by definition. The only thing which needs storing is the fact that there is some proof.

[Edward van de Meent]

well, i imagine storing it might make it slightly more efficient if you'd like to know what axioms you used after the fact, but that's hardly a main feature of the system. so it isn't exactly like there's no point, but the benefits are far outweighed by the downsides

[Preeyan Parmar]

That's 1. answered. Many thanks.

I've made some progress on 5. I needed to change the signature of right_hand_step a bit:

def right_hand_step {R: Relation α} {x y: α} (hxy : TClos R x y) : {z : α} → R y z → TClos R x z :=
  .rec
    (fun hxy hyz => .step hxy (.base hyz))
    (fun hxw _ ih hyz => .step hxw (ih hyz))
    hxy

I'm not sure why, but I can't move {z : \alpha} to the left of the colon, nor hxy to the right of the colon, without getting errors.

I can satisfy the original signature of right_hand_step like this:

def right_hand_step {R: Relation α} {x y z: α} : TClos R x y → R y z → TClos R x z :=
  let temp (hxy : TClos R x y) : (z : α) → R y z → TClos R x z :=
    .rec
      (fun hxy _ hyz => .step hxy (.base hyz))
      (fun hxw _ ih z hyz => .step hxw (ih z hyz))
      hxy
  fun hxy hyz => temp hxy z hyz

However, I've had to make the z variable explicit (I don't know why) and also I haven't found a way to do this without the let - I would have thought that I could just substitute the definition of temp.

[Mario Carneiro]

Note that lean does store the bodies of theorems currently; otherwise #print on a theorem wouldn't work (nor #print axioms as mentioned above, although you can precalculate this)

[Mario Carneiro]

there have been discussions about pruning them in at least some compilation modes though

[Mario Carneiro]

Regarding question 4, you can set the intermediate variable to have name w like this:

def right_hand_step {R: Relation α} {x y z: α} : TClos R x y → R y z → TClos R x z
  | .base hxy, hyz => .step hxy (.base hyz)
  | .step (y := w) hxw hwy, hyz => .step hxw (right_hand_step hwy hyz)

although this doesn't fix the issue with the recursion

[Mario Carneiro]

regarding 5, the more usual way to write T.rec functions without mentioning T is using the (e).rec form, because T.rec takes an argument of type T, it doesn't return one (in general); in this case it does which is why you can use the .rec form but I think this comes too late to resolve the implicit argument z. This works:

def right_hand_step {R: Relation α} {x y z: α} (hxy : TClos R x y) : R y z → TClos R x z :=
  hxy.rec
    (fun hxy hyz => .step hxy (.base hyz))
    (fun hxw _ ih hyz => .step hxw (ih hyz))

[Mario Carneiro]

By the way you can see how this is done in mathlib - docs#Relation.TransGen.trans_left - and it uses induction similar to your Q4

[Preeyan Parmar]

Many thanks @Mario Carneiro !

3. --> makes complete sense, of course the type here is just an implicit argument to TClos.step and it can be passed explicitly as you say
4. Cool, makes sense.
5. I don't understand how hxy.rec works because https://lean-lang.org/functional_programming_in_lean/getting-to-know/structures.html says "If TARGET has type T, the function named T.f is called", but doesn't hxy have type TClos R x y (which evaluates to Prop?) and isn't the recursor named TClos.rec ?

[Ruben Van de Velde]

5. So f is rec, TARGET is hxy of type T = TClos so TClos.rec is called? I don't see the mismatch

[Preeyan Parmar]

Why does (hxy : TClos R x y) not mean that the type of hxy is TClos R x y ?

[Ruben Van de Velde]

What makes you say it isn't?

[Ruben Van de Velde]

Or do you mean the arguments to TClos are confusing you?

[Preeyan Parmar]

I don't understand the sense in which hxy has type TClos. (For example, if I had an f : TClos -> Nat could I form f hxy?)

(There's a chance I'm missing something silly here...)

[Preeyan Parmar]

Having played around a bit, I think the bit I'm missing is something like:

• type constructors are not functions Type --> Type (they are more like syntactic extensions)
• in particular, type constructors are not types (TClos is not a type)
• but people still call it a type for convenience (and everyone knows what is meant (except me :)))

[Preeyan Parmar]

(And I think my original question 2. is answered by https://lean-lang.org/functional_programming_in_lean/monads/conveniences.html#leading-dot-notation)

[Mario Carneiro]

@Preeyan Parmar said:

I don't understand the sense in which hxy has type TClos. (For example, if I had an f : TClos -> Nat could I form f hxy?)

(There's a chance I'm missing something silly here...)

Ruben was being imprecise to say that hxy has type TClos. It actually has type TClos R x y, TClos is not a type it is a type operator. But the rule for dot-notation resolution says that hxy.foo will call T.foo where T is the name of the constant symbol at the head of the application of the type of hxy, which in this case is TClos. (That is, take the type of hxy, throw away the arguments and look at the name of the head constant.)

[Mario Carneiro]

Preeyan Parmar said:

• type constructors are not functions Type --> Type (they are more like syntactic extensions)

No, type constructors are functions Type -> Type, or more generally functions of multiple arguments returning Sort u for some u. TClos has type {α: Type} → Relation α → α → α → Prop, where Prop is Sort 0.

[Mario Carneiro]

Your other assertions are correct: TClos is not a type but people use TClos as shorthand for TClos .., i.e. the type TClos R a b for some R, a, b.

[Preeyan Parmar]

Crystal clear, thanks Mario!