Induction

Stream: new members

[Patrick Thomas]

Suppose I have the following:

namespace lambda

inductive exp : Type
| var : string → exp
| app : exp → exp → exp
| abs : string → exp → exp

inductive is_subterm : exp → exp → Prop
-- x ∈ Sub (x)
| var : ∀ (x : string), is_subterm (exp.var x) (exp.var x)

-- e1 ∈ Sub ((e1 e2))
| app_l : ∀ (e1 : exp) (e2 : exp), is_subterm e1 (exp.app e1 e2)

-- e2 ∈ Sub ((e1 e2))
| app_r : ∀ (e1 : exp) (e2 : exp), is_subterm e2 (exp.app e1 e2)

-- (e1 e2) ∈ Sub ((e1 e2))
| app_self : ∀ (e1 : exp) (e2 : exp), is_subterm (exp.app e1 e2) (exp.app e1 e2)

-- e ∈ Sub ((λ x . e))
| abs : ∀ (x : string) (e : exp), is_subterm e (exp.abs x e)

-- (λ x . e) ∈ Sub ((λ x . e))
| abs_self : ∀ (x : string) (e : exp), is_subterm (exp.abs x e) (exp.abs x e)

Is it possible to prove that is_subterm does not hold for something? For example, could one prove that if x is a lambda variable, then the only subterm of x is x itself?

[Patrick Massot]

Doesn't it contradict is_subterm.abs?

[Patrick Thomas]

Are you saying that the statement "if x is a lambda variable, then the only subterm of x is x itself", does not hold because of is_subterm.abs? I'm not sure I see why that would be the case?

[Gabriel Ebner]

This is provable (hint: try the cases tactic):

example (y x) : is_subterm y (exp.var x) → y = exp.var x

[Rob Lewis]

You may need to be a little careful about how you state it, but this is a good place to take advantage of the equation compiler. It will discharge the structurally impossible cases for you.

example (s : string) : ∀ (e : exp), is_subterm e (exp.var s) → e = exp.var s
| _ (is_subterm.var _) := rfl

(As Gabriel points out, cases will do the same thing.)

[Patrick Massot]

oh I missed "variable" in "lambda variable", it's on the next line here

[Patrick Thomas]

Thank you. I will have to do some reading on tactics and the equation compiler.

[Patrick Thomas]

I'm still learning how induction is handled in Lean. Does the inductive definition create theorems related to what is not an object of the defined type?

[Rob Lewis]

The only objects of the defined type are the ones that can be defined using the constructors. This is a "theorem" that's captured by the type's induction principle. In your case, look at #check is_subterm.cases_on .

[Kenny Lau]

should we use nat instead of string?

[Patrick Thomas]

Is the following what Gabriel means by the cases tactic?

example (e : exp) (x : string) : is_subterm e (exp.var x) → e = exp.var x :=
    exp.cases_on e
    (show ∀ (y : string), is_subterm (exp.var y) (exp.var x) → (exp.var y) = (exp.var x), from
    assume y : string,

I'm not sure how to proceed from here.

[Kenny Lau]

well by the cases tactic he means by cases e

[Kenny Lau]

but I don't know if you're familiar with using tactics

[Patrick Thomas]

Oh. No, I'm not.

[Gabriel Ebner]

Actually I mean by cases on the is_subterm proof:
begin intro h, cases h, end (you can easily solve the remaining goal)

[Kenny Lau]

why bother making is_subterm inductive

[Patrick Thomas]

I thought it would have to be. What is the alternative?

[Kenny Lau]

well it isn't inductive (i.e. recursive) so maybe just make it a def or something

[Patrick Thomas]

Hmm. I was trying to formalize the recursive definition of the set of all subterms of a lambda expression given by definition 1.3.5 here: https://play.google.com/books/reader?id=orsrBQAAQBAJ&hl=en_US&pg=GBS.PA5.w.4.0.36
Did I do this wrong?

[Rob Lewis]

You're missing the recursive calls. The set of subterms of (M N) is the union of the subterms of M, the subterms of N, and the singleton set {(M N)}.

[Rob Lewis]

In your definition, (M N) only has three subterms: M, N, and (M N).

[Rob Lewis]

This is a perfectly good situation to use an inductive predicate, but the one you wrote isn't the one you wanted.

[Patrick Thomas]

Does adding the following fix it?

| app_l' : ∀ (e : exp) (e1 : exp) (e2 : exp), (is_subterm e e1) → is_subterm e (exp.app e1 e2)
| app_r' : ∀ (e : exp) (e1 : exp) (e2 : exp), (is_subterm e e2) → is_subterm e (exp.app e1 e2)
| abs' : ∀ (e : exp) (x : string) (e1 : exp), (is_subterm e e1) → is_subterm e (exp.abs x e1)

Also, is there a way to formalize this as a set, similar to the definition in the book?

[Gabriel Ebner]

Sure, you can just write a recursive function:

def subterms : exp → multiset exp
| (exp.var x) := {exp.var x}
-- ...

I'm not sure why they use multisets instead of sets though.

[Rob Lewis]

You could add those, and you can also reduce some of the others into one case.

inductive is_subterm : exp → exp → Prop
| self : ∀ x, is_subterm x x
| app_l : ∀ e₁ e₂ x, is_subterm x e₁ → is_subterm x (exp.app e₁ e₂)
| app_r : ∀ e₁ e₂ x, is_subterm x e₂ → is_subterm x (exp.app e₁ e₂)
| abs : ∀ e s x, is_subterm x e → is_subterm x (exp.abs s e)

[Kenny Lau]

and rename self into refl...

[Kenny Lau]

def is_subterm : exp → exp → bool
| e (exp.var s) := e = exp.var s
| e (exp.app e₁ e₂) := (e = exp.app e₁ e₂) || is_subterm e e₁ || is_subterm e e₂
| e (exp.abs s e') := (e = exp.abs s e') || is_subterm e e'

[Kenny Lau]

def is_subterm (e : exp) : exp → bool
| (exp.var s) := e = exp.var s
| (exp.app e₁ e₂) := (e = exp.app e₁ e₂) || is_subterm e₁ || is_subterm e₂
| (exp.abs s e') := (e = exp.abs s e') || is_subterm e'

[Patrick Thomas]

@Gabriel Ebner Cool. Could something similar be done for the set of all lambda terms?

[Patrick Thomas]

I was wondering what the error "nested occurrence 'and (sub_is_def P x N) (not (has_mem.mem.{0 0} var (set.{0} var) (set.has_mem.{0} var) y (FV N)))' contains variables that are not parameters" means in the last definition of:

inductive var : Type

inductive pre_term : Type
| var : var -> pre_term
| app : pre_term -> pre_term -> pre_term
| abs : var -> pre_term -> pre_term

def FV : pre_term -> set var
| ( pre_term.var x ) := { x }
| ( pre_term.app P Q ) := FV ( P ) ∪ FV ( Q )
| ( pre_term.abs x P ) := FV ( P ) \ { x }

inductive sub_is_def : pre_term -> var -> pre_term -> Prop
| var_same :
    forall ( y : var ) ( x : var ) ( N : pre_term ),
    ( x = y ) -> sub_is_def ( pre_term.var y ) x N
| var_diff :
    forall ( y : var ) ( x : var ) ( N : pre_term ),
    not ( x = y ) -> sub_is_def ( pre_term.var y ) x N
| app :
    forall ( P : pre_term ) ( Q : pre_term ) ( x : var ) ( N : pre_term ),
    sub_is_def P x N -> sub_is_def Q x N -> sub_is_def ( pre_term.app P Q ) x N
| abs_same :
    forall ( y : var ) ( P : pre_term ) ( x : var ) ( N : pre_term ),
    ( x = y ) -> sub_is_def ( pre_term.abs y P ) x N
| abs_diff :
    forall ( y : var ) ( P : pre_term ) ( x : var ) ( N : pre_term ),
    not ( x = y ) -> x ∉ FV ( pre_term.abs y P ) ∨ ( ( sub_is_def P x N ) ∧ ( y ∉ FV ( N ) ) ) -> sub_is_def ( pre_term.abs y P ) x N

It seems to be related to the /\ in abs_diff.

[Mario Carneiro]

sub_is_def is embedded in a complicated way in the last proposition

[Mario Carneiro]

you have to make it a manifestly positive occurrence:

inductive var : Type

inductive pre_term : Type
| var : var → pre_term
| app : pre_term → pre_term → pre_term
| abs : var → pre_term → pre_term

def FV : pre_term → set var
| (pre_term.var x) := {x}
| (pre_term.app P Q) := FV P ∪ FV Q
| (pre_term.abs x P) := FV P \ {x}

inductive sub_is_def : pre_term → var → pre_term → Prop
| var_same (x N) : sub_is_def (pre_term.var x) x N
| var_diff (y x N) : x ≠ y → sub_is_def (pre_term.var y) x N
| app {P Q x N} : sub_is_def P x N → sub_is_def Q x N → sub_is_def (P.app Q) x N
| abs_same (P x N) : sub_is_def (pre_term.abs x P) x N
| abs_diff_nel {x y P N} : x ≠ y → x ∉ FV P → sub_is_def (pre_term.abs y P) x N
| abs_diff {x y P N} : x ≠ y → y ∉ FV N → sub_is_def P x N → sub_is_def (pre_term.abs y P) x N

[Patrick Thomas]

Thank you. What does a "manifestly positive occurrence" mean?

[Mario Carneiro]

The definition of an inductive specification in lean requires that all constructors for the inductive type T have the form A1 -> A2 -> ... -> T where each A that mentions T has the form B1 -> B2 -> ... T (ignoring indexes). In other words, the only places the type T is allowed to appear is on the far right hand side (the constructor should produce an element of type T), and on the right of the left hand side (the constructors may take arguments of type T or arguments that are functions producing T). This is called "strict positivity". T is not allowed to appear anywhere else, so mk : (T -> A) -> T is not allowed, nor is mk : ((T -> A) -> A) -> T or foo T -> T or A /\ (T \/ B) -> T. The last two cases are called nested inductive types, and lean can sometimes compile them to primitive inductive types, but they aren't built in.

[Patrick Thomas]

I think I sort of understand. Thank you.

[Patrick Thomas]

Is it possible to have conditions in the constructors for inductively defined functions? For example, how would one define the lambda substitution x [ y := N ], which depends on whether x = y or x != y?

[Mario Carneiro]

you can use if

[Patrick Thomas]

Is there a description of using if in the doc?

[Mario Carneiro]

if p then a else b returns a if p is true and b if false

[Mario Carneiro]

In inductive predicates like the above, it's a bit nicer to have separate constructors for the true and false cases, but for recursive functions we usually use if

[Patrick Thomas]

For this:

def sub : pre_term → var → pre_term → pre_term
| (pre_term.var y) x N := if (pre_term.var x) = (pre_term.var y) then N else (pre_term.var y)

I get:
failed to synthesize type class instance for
sub : pre_term → var → pre_term → pre_term,
y x : var,
N : pre_term
⊢ decidable (pre_term.var x = pre_term.var y)

[Mario Carneiro]

you can say if x = y then ...

[Patrick Thomas]

I see. I still get the same error.

[Mario Carneiro]

What is var?

[Patrick Thomas]

inductive var : Type

[Mario Carneiro]

there are no vars?

[Patrick Thomas]

I'm not sure what you mean?

[Mario Carneiro]

that declaration means var is empty

[Mario Carneiro]

you can put @[derive decidable_eq] to automatically derive a decidable instance for var

[Patrick Thomas]

Oh. Should I have defined var differently?

[Mario Carneiro]

what do you want it to be? One reasonable choice is def var := nat

[Patrick Thomas]

I'm not sure. What would make the most sense for the lambda calculus? Maybe a character or a string?

[Mario Carneiro]

that works too

[Mario Carneiro]

But you have to be careful with how you handle bound variable renaming if you don't use de bruijn indices

[Mario Carneiro]

for example, subst can either rename variables, or it can be partial

[Mario Carneiro]

having it be a char seems like a bad idea because if the set of variables is finite then weird things happen

[Patrick Thomas]

I think it is partial in the book I am following for this. That is, it only defines substitution if it is capture avoiding.

[Mario Carneiro]

if your book uses explicit names then string works

[Mario Carneiro]

but you will need to prove a renaming lemma at some point, which will require you to know that var is infinite

[Patrick Thomas]

Ah. yes.

[Patrick Thomas]

I changed to def var := string.
If I have:

def sub : pre_term → var → pre_term → pre_term
| (pre_term.var y) x N := if x = y then N else y

Then I get:
type mismatch at application
ite (x = y) N y
term
y
has type
var
but is expected to have type
pre_term
If I go back to

def sub : pre_term → var → pre_term → pre_term
| (pre_term.var y) x N := if (pre_term.var x) = (pre_term.var y) then N else (pre_term.var y)

Then I still get:
failed to synthesize type class instance for
sub : pre_term → var → pre_term → pre_term,
y x : var,
N : pre_term
⊢ decidable (pre_term.var x = pre_term.var y)

[Patrick Thomas]

I see. I still needed @[derive decidable_eq].

[Patrick Thomas]

I get the same kind of error for

| (pre_term.app P Q) x N := if sub_is_def P x N ∧ sub_is_def Q x N then ( pre_term.app (sub P x N) (sub Q x N) )

failed to synthesize type class instance for
sub : pre_term → var → pre_term → pre_term,
P Q : pre_term,
x : var,
N : pre_term
⊢ decidable (sub_is_def P x N ∧ sub_is_def Q x N)

[Mario Carneiro]

def sub : pre_term → var → pre_term → pre_term
| (pre_term.var y) x N := if x = y then N else y

you are getting a type error because of the y at the end

[Mario Carneiro]

| (pre_term.app P Q) x N := if sub_is_def P x N ∧ sub_is_def Q x N then ( pre_term.app (sub P x N) (sub Q x N) )

Here you don't want to have the if at all. You have already defined the domain of definition of sub, so here you can just do the easy thing -

| (pre_term.app P Q) x N := pre_term.app (sub P x N) (sub Q x N)

[Mario Carneiro]

Alternatively, you can have sub itself be a (partial) functional relation rather than a recursive function

[Mario Carneiro]

that is, define $P[x:=N]=Q$ as an inductive predicate on four arguments

[Mario Carneiro]

inductive is_subst : pre_term → var → pre_term → pre_term → Prop
| var_same (x N) : is_subst (pre_term.var x) x N N
| var_diff (y x N) : x ≠ y → is_subst (pre_term.var y) x N (pre_term.var y)
| app {P Q x N P' Q'} : is_subst P x N P' → is_subst Q x N Q'  → is_subst (P.app Q) x N (P'.app Q')
| abs_same (P x N) : is_subst (pre_term.abs x P) x N (pre_term.abs x P)
| abs_diff_nel {x y P N} : x ≠ y → x ∉ FV P → is_subst (pre_term.abs y P) x N (pre_term.abs y P)
| abs_diff {x y P N P'} : x ≠ y → y ∉ FV N → is_subst P x N P' → is_subst (pre_term.abs y P) x N (pre_term.abs y P')

[Patrick Thomas]

Are you saying that whether P x N and Q x N are defined is already somehow part of the definition of sub?

[Mario Carneiro]

I suspect that it will be easier to work with the relation "the substitution of N for x in P is Q" rather than the conjunction of "the substitution is defined" and "the substitution is Q"

[Patrick Thomas]

I have been attempting to follow how the book I am going through does it, so that I can prove the theorems in the same manner. I want to improve the readability of the book for myself and others.

[Patrick Thomas]

It's a little circular. Reading the book to learn about the theory behind Lean, and using Lean to learn the book.

[Patrick Thomas]

In this instance I am formalizing the result of this question: https://math.stackexchange.com/questions/3109334/formal-definition-of-substitution-being-defined-in-type-free-lambda-calculus?noredirect=1&lq=1

[Patrick Thomas]

In the case of

| (pre_term.app P Q) x N := pre_term.app (sub P x N) (sub Q x N)

what will happen if I pass a pre_term for P or Q to the function for which the substitution is not defined?

[Mario Carneiro]

you get garbage

[Mario Carneiro]

but you get garbage no matter what with the "total function" / "domain of definition" approach

[Mario Carneiro]

The four place relation avoids this

[Patrick Thomas]

I see. I still hate to depart from the book, since many of the proofs involve showing that a given substitution is defined.

[Patrick Thomas]

I think using:

def var := string
@[derive decidable_eq]

inductive pre_term : Type
| var : var → pre_term
| app : pre_term → pre_term → pre_term
| abs : var → pre_term → pre_term

def FV : pre_term → set var
| (pre_term.var x) := {x}
| (pre_term.app P Q) := FV P ∪ FV Q
| (pre_term.abs x P) := FV P \ {x}

inductive sub_is_def : pre_term → var → pre_term → Prop
| var_same (x N) : sub_is_def (pre_term.var x) x N
| var_diff (y x N) : x ≠ y → sub_is_def (pre_term.var y) x N
| app {P Q x N} : sub_is_def P x N → sub_is_def Q x N → sub_is_def (P.app Q) x N
| abs_same (P x N) : sub_is_def (pre_term.abs x P) x N
| abs_diff_nel {x y P N} : x ≠ y → x ∉ FV P → sub_is_def (pre_term.abs y P) x N
| abs_diff {x y P N} : x ≠ y → y ∉ FV N → sub_is_def P x N → sub_is_def (pre_term.abs y P) x N

def sub : pre_term → var → pre_term → pre_term
| (pre_term.var y) x N := if x = y then N else (pre_term.var y)
| (pre_term.app P Q) x N := pre_term.app (sub P x N) (sub Q x N)
| (pre_term.abs y P) x N := if x = y then (pre_term.abs y P) else (pre_term.abs y (sub P x N))

may be closest to what they have.

[Patrick Thomas]

Although, yes, I guess keeping sub_is_def and adding the four place relation is about the same.

[Patrick Thomas]

What does the syntax (P.app Q)mean? Why that and not (pre_term.app P Q)?

[Bryan Gin-ge Chen]

I think this is an example of "dot notation". There's a thread on it here: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/dot.20notation.20confusion

[Patrick Thomas]

Thank you.

[Patrick Thomas]

I was wondering if someone would mind showing me how to set up the form of proof for the last lemma here (lemma_1_2_5_i). I'm pretty sure I want to do induction on M, but I'm having difficulty figuring out the syntax.

import data.set
open set

def var := ℕ
@[derive decidable_eq]

inductive pre_term : Type
| var : var → pre_term
| app : pre_term → pre_term → pre_term
| abs : var → pre_term → pre_term

def FV : pre_term → set var
| (pre_term.var x) := {x}
| (pre_term.app P Q) := FV P ∪ FV Q
| (pre_term.abs x P) := FV P \ {x}


lemma lemma_1 {α : Type} {s t : set α} {x : α} : x ∉ s → x ∉ s \ t :=
assume a1 : x ∉ s,
have s1 : x ∈ s \ t → x ∈ s, from set.mem_of_mem_diff,
have s2 : x ∉ s → x ∉ s \ t, from mt s1,
show x ∉ s \ t, from s2 a1


lemma lemma_2 {α : Type} {s t : set α} {x : α} : x ∉ s \ t → x ∉ t → x ∉ s :=
assume a1 : x ∉ s \ t,
assume a2 : x ∉ t,
have s1 : x ∈ s \ t ↔ x ∈ s ∧ x ∉ t, from set.mem_diff x,
have s2 : x ∈ s ∧ x ∉ t → x ∈ s \ t, from s1.elim_left,
have s3 : x ∉ s \ t → ¬ (x ∈ s ∧ x ∉ t), from mt s2,
have s4 : ¬ (x ∈ s ∧ x ∉ t), from s3 a1,
show x ∉ s, from not_and'.elim_left s4 a2


lemma lemma_3 (y : var) (P : pre_term) (x :var ) : x ∉ FV P → x ∉ FV (pre_term.abs y P) :=
assume a1 : x ∉ FV P,
have s1 : x ∉ FV P \ {y}, from lemma_1 a1,
show x ∉ FV (pre_term.abs y P), from s1


lemma lemma_4 (y : var) (P : pre_term) (x : var) : x ∉ FV (pre_term.abs y P) → x ≠ y → x ∉ FV P :=
assume a1 : x ∉ FV (pre_term.abs y P),
assume a2 : x ≠ y,
have s1 : x ∉ FV P \ {y}, from a1,
have s2 : x ∉ {y}, from mt set.mem_singleton_iff.elim_left a2,
show x ∉ FV P, from lemma_2 s1 s2


-- M [ x := N ]
inductive sub_is_def : pre_term → var → pre_term → Prop
| var_same (x N) : sub_is_def (pre_term.var x) x N
| var_diff (y x N) : x ≠ y → sub_is_def (pre_term.var y) x N
| app {P Q x N} : sub_is_def P x N → sub_is_def Q x N → sub_is_def (pre_term.app P Q) x N
| abs_same (P x N) : sub_is_def (pre_term.abs x P) x N
| abs_diff_nel {x y P N} : x ≠ y → x ∉ FV (pre_term.abs y P) → sub_is_def (pre_term.abs y P) x N
| abs_diff {x y P N} : x ≠ y → y ∉ FV N → sub_is_def P x N → sub_is_def (pre_term.abs y P) x N

def sub : pre_term → var → pre_term → pre_term
| (pre_term.var y) x N := if x = y then N else (pre_term.var y)
| (pre_term.app P Q) x N := pre_term.app (sub P x N) (sub Q x N)
| (pre_term.abs y P) x N := if x = y then (pre_term.abs y P) else (pre_term.abs y (sub P x N))

inductive is_subst : pre_term → var → pre_term → pre_term → Prop
| var_same (x N) : is_subst (pre_term.var x) x N N
| var_diff (y x N) : x ≠ y → is_subst (pre_term.var y) x N (pre_term.var y)
| app {P Q x N P' Q'} : is_subst P x N P' → is_subst Q x N Q' → is_subst (pre_term.app P Q) x N (pre_term.app P' Q')
| abs_same (P x N) : is_subst (pre_term.abs x P) x N (pre_term.abs x P)
| abs_diff_nel {x y P N} : x ≠ y → x ∉ FV (pre_term.abs y P) → is_subst (pre_term.abs y P) x N (pre_term.abs y P)
| abs_diff {x y P N P'} : x ≠ y → y ∉ FV N → is_subst P x N P' → is_subst (pre_term.abs y P) x N (pre_term.abs y P')


lemma lemma_1_2_5_i (M : pre_term) (x : var) (N : pre_term) : x ∉ FV M → sub_is_def M x N :=
assume a1 : x ∉ FV M,
show sub_is_def M x N, from sorry

[Chris Hughes]

This is one way. Your induction hypothesis will be called lemma_1_2_5_i

lemma lemma_1_2_5_i : ∀ (M : pre_term) (x : var) (N : pre_term), x ∉ FV M → sub_is_def M x N
| (pre_term.var v) := λ x N h, sorry
| (pre_term.app a b) := λ x N h, sorry
| (pre_term.abs a b) := λ x N h, sorry

[Mario Carneiro]

Are you familiar with tactic proofs? It's a bit easier to handle these big inductive predicates using induction

[Mario Carneiro]

something like this:

lemma lemma_1_2_5_i (M : pre_term) (x : var) (N : pre_term) (a1 : x ∉ FV M) : sub_is_def M x N :=
begin
  induction M,
  case pre_term.var {
    by_cases x = M,
    { subst h, constructor },
    { constructor, assumption } },
  case pre_term.app : M₁ M₂ IH₁ IH₂ {
    constructor,
    { apply IH₁, simp [FV] at a1, tauto },
    { apply IH₂, simp [FV] at a1, tauto } },
  case pre_term.abs : y M IH {
    by_cases x = y,
    { subst h, constructor },
    { exact sub_is_def.abs_diff_nel h a1 } }
end

[Patrick Thomas]

Mario: No, not that familiar. I'll have to look these commands up. Thank you.
Chris: What does the h in each case correspond to?

[Johan Commelin]

@Patrick Thomas A proof that x ∉ FV M

[Patrick Thomas]

Ahh. Thank you.

[Patrick Thomas]

How would I match each case of the inductively defined proposition without tactics? For example:

example (M : var) (x : var) (N : pre_term) (h1 : x ∉ FV (pre_term.var M)) : sub_is_def (pre_term.var M) x N := sorry

[Patrick Thomas]

Actually, how are each of the cases in sub_is_def matched in the proof that Mario gave?

[Mario Carneiro]

The proof is by induction on M, not sub_is_def

[Mario Carneiro]

so there is one case for each constructor of pre_term

[Mario Carneiro]

But it is proving sub_is_def, and in most of the cases I use constructor to pick the appropriate constructor

[Patrick Thomas]

What does constructor do?

[Mario Carneiro]

it's basically apply sub_is_def.var_same <|> apply sub_is_def.var_diff <|> ...

[Patrick Thomas]

Interesting. Thank you.

[Patrick Thomas]

Does the use of the by_cases tactic mean that the proof requires classical reasoning?

[Fabian Glöckle]

The by_casestactic needs that the proposition is decidable, and tries to create such an instance by typeclass inference. Decidability can be proven within a theory (like the decidable equality of natin data/nat/basic.lean: instance : decidable_eq ℕ) or be assumed as a classical axiom. This is the line

local attribute [instance] classical.prop_decidable

you find in certain files.

[Patrick Thomas]

How is a function with if...then...else used? For example, how would one prove the example in the following:

def var := ℕ

inductive pre_term : Type
| var : var → pre_term
| app : pre_term → pre_term → pre_term
| abs : var → pre_term → pre_term

def sub : pre_term → var → pre_term → pre_term
| (pre_term.var y) x N := if x = y then N else (pre_term.var y)
| (pre_term.app P Q) x N := pre_term.app (sub P x N) (sub Q x N)
| (pre_term.abs y P) x N := if x = y then (pre_term.abs y P) else (pre_term.abs y (sub P x N))

variables x y : var
variable N : pre_term

example := x = y → sub (pre_term.var y) x N = N

[Simon Hudon]

split_ifs is your friend when you see ite or dite (the functions underneath the if _ then _ else _) in your goal

[Patrick Thomas]

I don't think I see ite or dite? Maybe the goal hasn't been broken down enough yet?

[Simon Hudon]

First unfold sub, then you'll see it

[Patrick Thomas]

I'm sorry, I'm new to tactics. Would you mind giving an example? I'd be curious how to use sub without tactics as well.

[Mario Carneiro]

without tactics:

example (h : x = y) : sub (pre_term.var y) x N = N := if_pos h

[Mario Carneiro]

with tactics:

example (h : x = y) : sub (pre_term.var y) x N = N :=
by {unfold sub, simp [h]}

[Patrick Thomas]

Thank you!

[Patrick Thomas]

How does the if_pos example know which constructor of sub to use? Can it be explicitly told?

[Patrick Thomas]

When I clicked on the Induction title it showed two threads, one named INduction at the top and the other named Induction after.

[Kevin Buzzard]

What's the if_pos example?

[Kevin Buzzard]

I don't understand your question.

[Kevin Buzzard]

You know you can hover on terms in VS Code to see their type? Does this sort of technique answer your question?

[Kevin Buzzard]

example : sub (pre_term.var y) x N = if x = y then N else (pre_term.var y) := rfl

Does that answer your question? The left hand side equals the if statement by definition.

[Patrick Thomas]

I guess I mean: What is being substituted for what in the definition of if_pos and how does it decide on those particular substitutions? Is there a way in Visual Studio to see what substitutions are being made?

[Alistair Tucker]

You mean the implicit arguments to if_pos? The stuff in curly brackets?

[Alistair Tucker]

example (h : x = y) : sub (pre_term.var y) x N = N := @if_pos (x = y) _ h pre_term N (pre_term.var y)

[Mario Carneiro]

How does the if_pos example know which constructor of sub to use? Can it be explicitly told?

sub doesn't have constructors - it's a recursive definition. So sub (pre_term.var y) x N and if x = y then N else (pre_term.var y) are the same thing from lean's point of view, there is no constructor application to turn one into the other, just definitional unfolding

[Kevin Buzzard]

example (h : x = y) : sub (pre_term.var y) x N = N := if_pos h

#check if_pos
/-
if_pos : ?M_1 → ∀ {α : Sort u_1} {t e : α}, ite ?M_1 t e = t
-/
#check @if_pos -- sometimes output is clearer
/-
if_pos : ∀ {c : Prop} [h : decidable c],
  c → ∀ {α : Sort u_1} {t e : α}, ite c t e = t
-/

example (h : x = y) : sub (pre_term.var y) x N = N := @if_pos _ _ h _ _ _

[Kevin Buzzard]

Of the five inputs to if_pos that you didn't give, four were worked out by just thinking about the types of things, and the value of h : decidable c was supplied by the type class inference system.

[Kevin Buzzard]

example (h : x = y) : sub (pre_term.var y) x N = N := @if_pos _ (by apply_instance) h _ _ _

[Patrick Thomas]

I think I understand now. Thank you!

[Patrick Thomas]

I was wondering if someone might be able to show me how to use the equalities sub P x N = P and sub Q x N = Q to show that pre_term.app (sub P x N) (sub Q x N) = pre_term.app P Q given

inductive pre_term : Type
| var : var → pre_term
| app : pre_term → pre_term → pre_term
| abs : var → pre_term → pre_term

def sub : pre_term → var → pre_term → pre_term
-- if x = y then y [ x := N ] = N else y [ x := N ] = y
| (pre_term.var y) x N := if (x = y) then N else (pre_term.var y)

-- (P Q) [ x := N ] = (P [ x := N ] Q [ x := N ])
| (pre_term.app P Q) x N := pre_term.app (sub P x N) (sub Q x N)

-- if x = y then ( λ y . P ) [ x := N ] = ( λ y . P ) else ( λ y . P ) [ x := N ] = ( λ y . P [ x := N ] )
| (pre_term.abs y P) x N := if x = y then (pre_term.abs y P) else (pre_term.abs y (sub P x N))

Thank you.

[Kevin Buzzard]

Can you post fully working code? It makes everyone's life easier.

[Patrick Thomas]

Sure, give me a second.

[Kevin Buzzard]

Can you formalise precisely what you want proved as well, rather than just describing it?

[Patrick Thomas]

I think this is a minimum working example:

def var := ℕ

inductive pre_term : Type
| var : var → pre_term
| app : pre_term → pre_term → pre_term
| abs : var → pre_term → pre_term

def sub : pre_term → var → pre_term → pre_term
-- if x = y then y [ x := N ] = N else y [ x := N ] = y
| (pre_term.var y) x N := if (x = y) then N else (pre_term.var y)

-- (P Q) [ x := N ] = (P [ x := N ] Q [ x := N ])
| (pre_term.app P Q) x N := pre_term.app (sub P x N) (sub Q x N)

-- if x = y then ( λ y . P ) [ x := N ] = ( λ y . P ) else ( λ y . P ) [ x := N ] = ( λ y . P [ x := N ] )
| (pre_term.abs y P) x N := if x = y then (pre_term.abs y P) else (pre_term.abs y (sub P x N))


example (P Q N : pre_term) (x : var) (h1 : sub P x N = P) (h2 : sub Q x N = Q) :
    pre_term.app (sub P x N) (sub Q x N) = pre_term.app P Q := sorry

[Kevin Buzzard]

example (P Q N : pre_term) (x : var) (h1 : sub P x N = P) (h2 : sub Q x N = Q) :
    pre_term.app (sub P x N) (sub Q x N) = pre_term.app P Q :=
begin
  rw h1,
  rw h2,
end

[Patrick Thomas]

Thank you. Do you mind showing how it might be done without tactics?

[Kevin Buzzard]

#print the proof term? :-/

[Kevin Buzzard]

or you could try the dreaded triangle

[Patrick Thomas]

Triangle?

[Kevin Buzzard]

\t

[Kevin Buzzard]

eq.subst

[Patrick Massot]

substituting in what?

[Kevin Buzzard]

it's a version of rw which works in term mode but never works for me.

[Patrick Massot]

in (rlf : pre_term.app P Q = pre_term.app P Q) maybe

[Kevin Buzzard]

substituting in what?

I dunno, I can never get it to work

[Patrick Massot]

Anyway, let's not encourage Patrick's masochism here

[Kevin Buzzard]

it won't work, it will change too many P's

[Patrick Massot]

@Patrick Thomas you really need to learn tactic mode

[Patrick Thomas]

I think it is more that I like it to be explicit. I guess in this case it is obvious enough.

[Kevin Buzzard]

def ABC (P Q N : pre_term) (x : var) (h1 : sub P x N = P) (h2 : sub Q x N = Q) :
    pre_term.app (sub P x N) (sub Q x N) = pre_term.app P Q :=
begin
  rw h1,
  rw h2,
end

#print ABC
/-
def ABC : ∀ (P Q N : pre_term) (x : var),
  sub P x N = P → sub Q x N = Q → pre_term.app (sub P x N) (sub Q x N) = pre_term.app P Q :=
λ (P Q N : pre_term) (x : var) (h1 : sub P x N = P) (h2 : sub Q x N = Q),
  eq.mpr (id (eq.rec (eq.refl (pre_term.app (sub P x N) (sub Q x N) = pre_term.app P Q)) h1))
    (eq.mpr (id (eq.rec (eq.refl (pre_term.app P (sub Q x N) = pre_term.app P Q)) h2)) (eq.refl (pre_term.app P Q)))
    -/

[Patrick Massot]

How nicely explicit!

[Patrick Thomas]

LOL

[Patrick Massot]

Maybe you can remove a couple of id and still be explicit enough

[Kevin Buzzard]

Take a look at mathlib. They love obfuscated one-line term mode proofs -- when they can get them to work. But there are plenty of times in mathlib when they go into tactic mode precisely for reasons such as this. In mathlib the proof would be by rw [h1, h2]. rw is a powerful tactic. Why try emulating it in term mode?

[Patrick Thomas]

Yeah, I think in this case I'll use the tactic.

[Patrick Massot]

Yes rw is the tactic mode reason number one in mathlib

[Kevin Buzzard]

Many of my tactic mode proofs are rw this, change that, rw this, change that, rwa this

[Kevin Buzzard]

As Patrick says, it's the number one reason to go into tactic mode.

[Kevin Buzzard]

At least for me. If I could use simp better then this might not be the case -- I am slowly learning how to use it.

[Kevin Buzzard]

def ABC (P Q N : pre_term) (x : var) (h1 : sub P x N = P) (h2 : sub Q x N = Q) :
    pre_term.app (sub P x N) (sub Q x N) = pre_term.app P Q :=
have H : pre_term.app (sub P x N) Q = pre_term.app P Q, from h1.symm ▸ rfl,
h2.symm ▸ H

Triangle level up

[Kevin Buzzard]

def ABC (P Q N : pre_term) (x : var) (h1 : sub P x N = P) (h2 : sub Q x N = Q) :
    pre_term.app (sub P x N) (sub Q x N) = pre_term.app P Q :=
h2.symm ▸ (h1.symm ▸ rfl)

Triangle master!

[Patrick Massot]

Hey, that was my proposal!

[Patrick Massot]

Patrick, do you really think this is more explicit than rw?

[Kevin Buzzard]

The symms are for some reason crucial

[Patrick Massot]

Ahh

[Kevin Buzzard]

and the rfl figured out its own type, to my surprise

[Patrick Massot]

I didn't try

[Kevin Buzzard]

but honestly, triangle does not scale :-/

[Kevin Buzzard]

Seems that the triangle by default picks up the first match shrug

[Patrick Thomas]

Patrick: I think the rewrite works well here. I haven't used tactics enough for it to have occurred to me.

[Andrew Ashworth]

If you want to get rid of the symms, you could try eq.substr

[Andrew Ashworth]

unfortunately it doesn't have the nice triangle notation like eq.subst does

[Patrick Thomas]

Given:

def var := ℕ

inductive pre_term : Type
| var : var → pre_term
| app : pre_term → pre_term → pre_term
| abs : var → pre_term → pre_term

def FV : pre_term → set var
| (pre_term.var x) := {x}
| (pre_term.app P Q) := (FV P) ∪ (FV Q)
| (pre_term.abs x P) := (FV P) \ {x}


-- sub_is_def M x N means M [ x := N ] is defined
inductive sub_is_def : pre_term → var → pre_term → Prop

-- y [ x := N ] is defined
| var (y : var) (x : var) (N : pre_term) :
  sub_is_def (pre_term.var y) x N

-- P [ x := N ] is defined → Q [ x := N ] is defined → (P Q) [ x := N ] is defined
| app (P : pre_term) (Q : pre_term) (x : var) (N : pre_term) :
  sub_is_def P x N → sub_is_def Q x N → sub_is_def (pre_term.app P Q) x N

-- x = y → ( λ y . P ) [ x := N ] is defined
| abs_same (y : var) (P : pre_term) (x : var) (N : pre_term) :
  x = y → sub_is_def (pre_term.abs y P) x N

-- x ≠ y → x ∉ FV ( λ y . P ) → ( λ y . P ) [ x := N ] is defined
| abs_diff_nel (y : var) (P : pre_term) (x : var) (N : pre_term) :
  x ≠ y → x ∉ FV (pre_term.abs y P) → sub_is_def (pre_term.abs y P) x N

-- x ≠ y → y ∉ FV ( N ) → P [ x := N ] is defined → ( λ y . P ) [ x := N ] is defined
| abs_diff (y : var) (P : pre_term) (x : var) (N : pre_term) :
  x ≠ y → y ∉ FV N → sub_is_def P x N → sub_is_def (pre_term.abs y P) x N


-- M [ x := N ]
def sub : pre_term → var → pre_term → pre_term
-- if x = y then y [ x := N ] = N else y [ x := N ] = y
| (pre_term.var y) x N := if (x = y) then N else (pre_term.var y)

-- (P Q) [ x := N ] = (P [ x := N ] Q [ x := N ])
| (pre_term.app P Q) x N := pre_term.app (sub P x N) (sub Q x N)

-- if x = y then ( λ y . P ) [ x := N ] = ( λ y . P ) else ( λ y . P ) [ x := N ] = ( λ y . P [ x := N ] )
| (pre_term.abs y P) x N := if x = y then (pre_term.abs y P) else (pre_term.abs y (sub P x N))

Is the only way to combine sub_is_def and sub to use:

-- is_sub M x N L means M [ x := N ] = L
inductive is_sub : pre_term → var → pre_term → pre_term → Prop

-- x = y → y [ x := N ] = N
| var_same (y : var) (x : var) (N : pre_term) :
  x = y → is_sub (pre_term.var y) x N N

-- x ≠ y → y [ x := N ] = y
| var_diff (y : var) (x : var) (N : pre_term) :
  x ≠ y → is_sub (pre_term.var y) x N (pre_term.var y)

-- P [ x := N ] = P' → Q [ x := N ] = Q' → (P Q) [ x := N ] = (P' Q')
| app (P : pre_term) (Q : pre_term) (x : var) (N : pre_term) (P' : pre_term) (Q' : pre_term) :
  is_sub P x N P' → is_sub Q x N Q' → is_sub (pre_term.app P Q) x N (pre_term.app P' Q')

-- x = y → ( λ y . P ) [ x := N ] = ( λ y . P )
| abs_same (y : var) (P : pre_term) (x : var) (N : pre_term) :
  x = y → is_sub (pre_term.abs y P) x N (pre_term.abs y P)

-- x ≠ y → x ∉ FV ( λ y . P ) → ( λ y . P ) [ x := N ] = ( λ y . P )
| abs_diff_nel (y : var) (P : pre_term) (x : var) (N : pre_term) :
  x ≠ y → x ∉ FV (pre_term.abs y P) → is_sub (pre_term.abs y P) x N (pre_term.abs y P)

-- x ≠ y → y ∉ FV ( N ) → P [ x := N ] = P' → ( λ y . P ) [ x := N ] = ( λ y . P' )
| abs_diff (y : var) (P : pre_term) (x : var) (N : pre_term) (P' : pre_term) :
  x ≠ y → y ∉ FV N → is_sub P x N P' → is_sub (pre_term.abs y P) x N (pre_term.abs y P')

I can not make sub a function only on the domain for which sub_is_def holds?

[Mario Carneiro]

You can make sub (M : pre_term) (x : var) (N : pre_term) : sub_is_def M x N -> pre_term, but I strongly recommend against it

[Patrick Thomas]

Why the recommendation against it?

[Patrick Thomas]

Should I be able to prove the following?

lemma sub_iff (x :var) (L M N : pre_term) : ( is_sub M x N L ) ↔ ( M [ x := N ] is_def ) ∧ ( M [ x := N ] = L )

Perhaps by induction on M?

[Mario Carneiro]

what does is_def mean in the first conjunct?

[Patrick Thomas]

Sorry, left out the notation:

notation M `[` x `:=` N `]` `is_def` := sub_is_def M x N
notation M `[` x `:=` N `]` := sub M x N

[Mario Carneiro]

wow that's an ambiguous notation

[Kevin Buzzard]

Why not just post your full working code?

[Mario Carneiro]

it's mostly the same as the code in this thread I think

[Patrick Thomas]

Yeah. Here it is

import data.set
open set


def var := ℕ

inductive pre_term : Type
| var : var → pre_term
| app : pre_term → pre_term → pre_term
| abs : var → pre_term → pre_term


def FV : pre_term → set var
| (pre_term.var x) := {x}
| (pre_term.app P Q) := (FV P) ∪ (FV Q)
| (pre_term.abs x P) := (FV P) \ {x}


-- sub_is_def M x N means M [ x := N ] is defined
inductive sub_is_def : pre_term → var → pre_term → Prop

-- y [ x := N ] is defined
| var (y : var) (x : var) (N : pre_term) :
  sub_is_def (pre_term.var y) x N

-- P [ x := N ] is defined → Q [ x := N ] is defined → (P Q) [ x := N ] is defined
| app (P : pre_term) (Q : pre_term) (x : var) (N : pre_term) :
  sub_is_def P x N → sub_is_def Q x N → sub_is_def (pre_term.app P Q) x N

-- x = y → ( λ y . P ) [ x := N ] is defined
| abs_same (y : var) (P : pre_term) (x : var) (N : pre_term) :
  x = y → sub_is_def (pre_term.abs y P) x N

-- x ≠ y → x ∉ FV ( λ y . P ) → ( λ y . P ) [ x := N ] is defined
| abs_diff_nel (y : var) (P : pre_term) (x : var) (N : pre_term) :
  x ≠ y → x ∉ FV (pre_term.abs y P) → sub_is_def (pre_term.abs y P) x N

-- x ≠ y → y ∉ FV ( N ) → P [ x := N ] is defined → ( λ y . P ) [ x := N ] is defined
| abs_diff (y : var) (P : pre_term) (x : var) (N : pre_term) :
  x ≠ y → y ∉ FV N → sub_is_def P x N → sub_is_def (pre_term.abs y P) x N

notation M `[` x `:=` N `]` `is_def` := sub_is_def M x N


-- M [ x := N ]
def sub : pre_term → var → pre_term → pre_term
-- if x = y then y [ x := N ] = N else y [ x := N ] = y
| (pre_term.var y) x N := if (x = y) then N else (pre_term.var y)

-- (P Q) [ x := N ] = (P [ x := N ] Q [ x := N ])
| (pre_term.app P Q) x N := pre_term.app (sub P x N) (sub Q x N)

-- if x = y then ( λ y . P ) [ x := N ] = ( λ y . P ) else ( λ y . P ) [ x := N ] = ( λ y . P [ x := N ] )
| (pre_term.abs y P) x N := if x = y then (pre_term.abs y P) else (pre_term.abs y (sub P x N))

notation M `[` x `:=` N `]` := sub M x N


-- is_sub M x N L means M [ x := N ] = L
inductive is_sub : pre_term → var → pre_term → pre_term → Prop

-- x = y → y [ x := N ] = N
| var_same (y : var) (x : var) (N : pre_term) :
  x = y → is_sub (pre_term.var y) x N N

-- x ≠ y → y [ x := N ] = y
| var_diff (y : var) (x : var) (N : pre_term) :
  x ≠ y → is_sub (pre_term.var y) x N (pre_term.var y)

-- P [ x := N ] = P' → Q [ x := N ] = Q' → (P Q) [ x := N ] = (P' Q')
| app (P : pre_term) (Q : pre_term) (x : var) (N : pre_term) (P' : pre_term) (Q' : pre_term) :
  is_sub P x N P' → is_sub Q x N Q' → is_sub (pre_term.app P Q) x N (pre_term.app P' Q')

-- x = y → ( λ y . P ) [ x := N ] = ( λ y . P )
| abs_same (y : var) (P : pre_term) (x : var) (N : pre_term) :
  x = y → is_sub (pre_term.abs y P) x N (pre_term.abs y P)

-- x ≠ y → x ∉ FV ( λ y . P ) → ( λ y . P ) [ x := N ] = ( λ y . P )
| abs_diff_nel (y : var) (P : pre_term) (x : var) (N : pre_term) :
  x ≠ y → x ∉ FV (pre_term.abs y P) → is_sub (pre_term.abs y P) x N (pre_term.abs y P)

-- x ≠ y → y ∉ FV ( N ) → P [ x := N ] = P' → ( λ y . P ) [ x := N ] = ( λ y . P' )
| abs_diff (y : var) (P : pre_term) (x : var) (N : pre_term) (P' : pre_term) :
  x ≠ y → y ∉ FV N → is_sub P x N P' → is_sub (pre_term.abs y P) x N (pre_term.abs y P')


lemma sub_iff (x :var) (L M N : pre_term) : ( is_sub M x N L ) ↔ ( M [ x := N ] is_def ) ∧ ( M [ x := N ] = L ) := sorry

[Mario Carneiro]

seems like this is the wrong question. The answer to "is this provable" is either "no you got the math wrong" or "yes this can be formalized"

[Kenny Lau]

what if the provability is independent of the Lean axioms? :P

[Patrick Thomas]

That would be good to know too :)

[Mario Carneiro]

do you bring that up in all your intro classes Kenny?

[Kevin Buzzard]

In maths it's very unlikely that something Kenny saw so far would be even close to being indepedent!

[Kevin Buzzard]

Maybe I mentioned CH but I bet that's it.

[Mario Carneiro]

well, as you know there are several independent statements "close to the surface" in lean because MLTT is underdetermined... but this is off topic

[Patrick Thomas]

I guess my question is, that it was suggested that I use is_sub instead of the other two, and I was wondering if that is equivalent. I thought maybe this lemma would show that it is, if it is true.

[Mario Carneiro]

it is true, unless there is some subtle bug in the inductives

[Patrick Thomas]

Ok, thank you. I will try to prove it. Probably induction on M?

[Mario Carneiro]

induction on the predicates

[Patrick Thomas]

Hmm, I'm not sure I am familiar with that form of induction.

[Patrick Thomas]

How would you set that up? Can you use the induction tactic?

[Kevin Buzzard]

Yes. If you have some hypothesis h whose type is an inductive type, then induction h will do some kind of induction on h.

[Patrick Thomas]

I guess that is not the case here? Mario suggested induction on the predicates. Maybe that means is_sub.rec_on?

[Kevin Buzzard]

If you are in tactic mode and have h : is_sub (pre_term.var M) x N L then cases h or induction h (or, better, cases h with AAA BBB CCC DDD EEE FFF GGG and then look at the types of what you ended up with and rename accordingly) should work just fine. Yes, they're just applying rec under the hood.

[Patrick Thomas]

Thank you!

[Patrick Thomas]

Should there be induction hypotheses, for instance for the is_sub.app case?

[Patrick Thomas]

I don't see any under the goal.

[Patrick Thomas]

Do I need to add an axiom to have ( is_sub M x N P ∧ is_sub M x N Q ) → P = Q?

[Kevin Buzzard]

You shouldn't ever have to add axioms.

[Patrick Thomas]

Do you know how I might be able to show this?

[Mario Carneiro]

induction on the first is_sub (generalizing Q), cases on the other

[Patrick Thomas]

Thank you. On the proof of the earlier correspondence between is_sub and sub, sub_is_def, when I use cases, I kind of expected induction hypotheses in the goals, but I don't see any. Am I missing something in my understanding of the proof, or in the use of cases?

[Mario Carneiro]

cases is like induction except there are no induction hypotheses

[Mario Carneiro]

if you need an IH (and you will in these proofs) use induction

[Patrick Thomas]

I see. That makes sense. Feeling kind of silly. Thank you.

[Patrick Thomas]

Nevermind.

[Mario Carneiro]

I fixed your formatting

import data.set.basic
open set
local attribute [instance, priority 0] classical.prop_decidable

def var := ℕ

inductive pre_term : Type
| var : var → pre_term
| app : pre_term → pre_term → pre_term
| abs : var → pre_term → pre_term

def FV : pre_term → set var
| (pre_term.var x) := {x}
| (pre_term.app P Q) := FV P ∪ FV Q
| (pre_term.abs x P) := FV P \ {x}

lemma lemma_1 {x : var} {P Q : pre_term} : x ∈ FV (pre_term.app P Q) ↔ x ∈ FV P ∨ x ∈ FV Q :=
have s1 : FV (pre_term.app P Q) = FV P ∪ FV Q, by refl,
have s2 : x ∈ FV (pre_term.app P Q) ↔ x ∈ FV P ∪ FV Q, from (ext_iff (FV (pre_term.app P Q)) (FV P ∪ FV Q)).elim_left s1 x,
have s3 : x ∈ FV P ∪ FV Q ↔ ((x ∈ FV P) ∨ (x ∈ FV Q)), from mem_union x (FV P) (FV Q),
iff_iff_eq.elim_right (eq.trans (iff_iff_eq.elim_left s2) (iff_iff_eq.elim_left s3))

lemma lemma_2 {x : var} {y : var} {P : pre_term} : x ∈ FV (pre_term.abs y P) ↔ x ∈ FV P ∧ x ≠ y :=
begin
have : x ∈ FV (pre_term.abs y P) ↔ (x ∈ FV P ∧ x ∉ { y }), from mem_diff x,
have : x ∉ { y } ↔ x ≠ y, from not_iff_not.elim_right mem_singleton_iff,
simp *
end


-- M [ x := N ]
def sub : pre_term → var → pre_term → pre_term
-- if x = y then y [ x := N ] = N else y [ x := N ] = y
| (pre_term.var y) x N := if (x = y) then N else (pre_term.var y)

-- (P Q) [ x := N ] = (P [ x := N ] Q [ x := N ])
| (pre_term.app P Q) x N := pre_term.app (sub P x N) (sub Q x N)

-- if x = y then (λ y . P) [ x := N ] = (λ y . P) else (λ y . P) [ x := N ] = (λ y . P [ x := N ])
| (pre_term.abs y P) x N := if x = y then (pre_term.abs y P) else (pre_term.abs y (sub P x N))


lemma lemma_3 {α : Type} {s t : set α} {x : α} : s = t → x ∈ s → x ∈ t :=
assume a1 : s = t,
assume a2 : x ∈ s,
show x ∈ t, from ((ext_iff s t).elim_left a1 x).elim_left a2

lemma lemma_1_2_5_ii {M : pre_term} {x : var} {N : pre_term} {z : var} :
z ∈ FV (sub M x N) ↔ (z ∈ FV M ∧ x ≠ z) ∨ (z ∈ FV N ∧ x ∈ FV M) :=
begin
  split,
  { intro a1,
    show (z ∈ FV M ∧ x ≠ z) ∨ (z ∈ FV N ∧ x ∈ FV M), sorry },
  { assume a1 : (z ∈ FV M ∧ x ≠ z) ∨ (z ∈ FV N ∧ x ∈ FV M),
    show z ∈ FV (sub M x N),
    induction M,
    case pre_term.var {
      sorry },
    case pre_term.app : P Q IH_1 IH_2 {
      sorry },
    case pre_term.abs : y P IH {
      have s1 : (z ∈ FV (pre_term.abs y P) ∧ x ≠ z) ∨ (z ∈ FV N ∧ x ∈ FV (pre_term.abs y P)), from a1,
      refine or.elim s1 sorry _,
      assume a2 : z ∈ FV N ∧ x ∈ FV (pre_term.abs y P),
      have s2 : z ∈ FV N := and.elim_left a2,
      have s3 : x ∈ FV (pre_term.abs y P) := and.elim_right a2,
      have s4 : x ∈ FV P ∧ x ≠ y := lemma_2.elim_left s3,
      have s5 : x ∈ FV P := and.elim_left s4,
      have s6 : z ∈ FV N ∧ x ∈ FV P := and.intro s2 s5,
      have s7 : (z ∈ FV P ∧ x ≠ z) ∨ (z ∈ FV N ∧ x ∈ FV P) → z ∈ FV (sub P x N) := IH,
      have s8 : z ∈ FV (sub P x N) := s7 (or.inr s6),
      have s9 : x ≠ y := and.elim_right s4,
      have s5 : sub (pre_term.abs y P) x N = (pre_term.abs y (sub P x N)) := if_neg s9,
      show z ∈ FV (sub (pre_term.abs y P) x N),
      sorry } }
end

[Patrick Thomas]

The lemma won't work though right? Because I left out the hypothesis that M [ x := N ] is defined? Which is why I should use the is_sub definition?

[Mario Carneiro]

Here's my attempt at this lemma and the others leading up to it:

lemma lemma_1 {x : var} {P Q : pre_term} : x ∈ FV (pre_term.app P Q) ↔ x ∈ FV P ∨ x ∈ FV Q :=
mem_union _ _ _

lemma lemma_2 {x : var} {y : var} {P : pre_term} : x ∈ FV (pre_term.abs y P) ↔ x ∈ FV P ∧ x ≠ y :=
by simp [FV]

lemma lemma_3 {α : Type} {s t : set α} {x : α} (h : s = t) (hx : x ∈ s) : x ∈ t :=
h ▸ hx

lemma lemma_1_2_5_ii {M : pre_term} {x : var} {N : pre_term} {z : var} :
z ∈ FV (sub M x N) ↔ (z ∈ FV M ∧ x ≠ z) ∨ (z ∈ FV N ∧ x ∈ FV M) :=
begin
  induction M with y P Q IH_1 IH_2 y P IH; simp [sub, FV],
  { split_ifs,
    { subst x, simp [eq_comm] },
    { simp [h, FV], rw and_iff_left_of_imp,
      intro, subst z, exact h } },
  { simp [IH_1, IH_2, and_or_distrib_left,
      or_and_distrib_right, or.left_comm, or_assoc] },
  { split_ifs,
    { subst x, simp [eq_comm, and_assoc, FV] },
    { simp [FV, IH, h],
      by_cases zy : z = y,
      { subst z, simp, sorry },
      { simp [zy] } } }
end

[Mario Carneiro]

something goes wrong in the x != y, z = y case of abs

[Patrick Thomas]

Right. Because I left out the hypothesis that M [ x := N ] is defined? Which is why I should have used the is_sub definition?

[Mario Carneiro]

yes, that does the trick.

lemma sub_eq_self {M x N} (H : x ∉ FV M) : sub M x N = M :=
begin
  induction M with y P Q IH_1 IH_2 y P IH; simp [sub, FV] at H ⊢,
  { simp [H] },
  { simp [not_or_distrib] at H, exact H.imp IH_1 IH_2 },
  { split_ifs,
    { simp },
    { exact ⟨rfl, IH (mt H h)⟩ } }
end

lemma lemma_1_2_5_ii {M x N z} (H : sub_is_def M x N) :
  z ∈ FV (sub M x N) ↔ (z ∈ FV M ∧ x ≠ z) ∨ (z ∈ FV N ∧ x ∈ FV M) :=
begin
  induction H; simp [sub, FV],
  case sub_is_def.var : y x N {
    split_ifs,
    { subst x, simp [eq_comm] },
    { simp [h, FV], rw and_iff_left_of_imp,
      intro, subst z, exact h } },
  case sub_is_def.app : P Q x N _ _ IH1 IH2 {
    simp [IH1, IH2, and_or_distrib_left,
      or_and_distrib_right, or.left_comm, or_assoc] },
  case sub_is_def.abs_same : y P x N e {
    subst y, simp [eq_comm, and_assoc, FV] },
  case sub_is_def.abs_diff_nel : y P x N h hx {
    simp [FV, h] at hx ⊢,
    simp [sub_eq_self hx, hx],
    rw @and_iff_left_of_imp (_∧_),
    rintro ⟨h, _⟩ rfl, contradiction },
  case sub_is_def.abs_diff : y P x N h hy H IH {
    simp [FV, IH, h],
    by_cases zy : z = y; simp [zy, hy] }
end

[Patrick Thomas]

Thank you!

[Patrick Thomas]

Does this only use induction on H and no induction on M?

[Patrick Thomas]

What is the principle behind the induction on H? Would anyone have a recommendation for a resource describing this form of induction in general? How are the induction hypotheses determined?

[Kevin Buzzard]

If H is an inductive type, then Lean reads off the so-called recursor from the constructors of the type.

[Kevin Buzzard]

A good example to think about is nat. It's defined as: zero is a nat, the successor of a nat is a nat, and that's it. So the recursor is "if you can prove it for zero, and prove it for successors given a proof for all their inputs, you're done."

[Kevin Buzzard]

Another good example is false, the inductive proposition with no constructors. Because there are no constructors, the inductive principle is "you don't have to check anything and you can get a map from false to P for free", i.e. the statement that false implies P for all propositions P.

[Kevin Buzzard]

Maybe read TPIL, the chapter on inductive types?

[Kevin Buzzard]

I was really excited when I realised that one could do induction on the reals in Lean! And then it turned out that the theorem was: "if you can prove it for all Cauchy sequences of rationals, you can deduce it for all reals"!

[Patrick Thomas]

In this case H is not a type though right? It is a predicate?

[Kevin Buzzard]

A predicate can be an inductive type

[Kevin Buzzard]

I'm talking about the recursor attached to a general inductive type. You can do induction on an inductive type and the recursor is the function which does it for you

[Kevin Buzzard]

I think you can also do induction on a quotient type, you just end up doing things on the bigger type and checking they're constant on equivalence classes

[Kevin Buzzard]

You can't do induction on a pi type, and that's all the types there is

[Kevin Buzzard]

Apart from universes, if you want to call theem types, and you can't do induction on them either

[Patrick Thomas]

What is the principle for the recursor for an inductive type that is a predicate, in non formal terms? Is there a simple example like nat, but for a predicate?

[Kevin Buzzard]

Just make a simple inductive predicates called X and then do #check @X.rec

[Kevin Buzzard]

And and or are good ones

[Kevin Buzzard]

I'm on a bus right now with no access to lean. Aren't these things talked about in TPIL? there's an interesting treatment of them in that coq book logical foundations

[Patrick Thomas]

I may have to go back through the section in TPIL. I was looking for other introductory resources as well.

[Kevin Buzzard]

Try and figure out what the recursors for and and or are and then check in Lean.

[Patrick Thomas]

Is there a way to combine the following into a single justification for the second line?

have s3 : FV ( sub ( pre_term.var y ) x N ) = FV ( N ), by rw s2,
have s4 : z ∈ FV ( N ), from s3 ▸ a2,

[Kevin Buzzard]

have s4 : z ∈ FV ( N ), from (show FV ( sub ( pre_term.var y ) x N ) = FV ( N ), by rw s2) ▸ a2, might work