## Stream: new members

### Topic: terms as types?

#### Alexandre Rademaker (Sep 04 2019 at 12:23):

We can prove a formula from assumptions declared as parameters:

variables A B : Prop
example (h₂ : A ∧ B): A := h₂.left


We can also reuse the parameters declaring them as variables:

variable h₂ : A ∧ B
example : A := and.left h₂


Now imagine that we want to prove the same formula in different many ways using different assumptions. Say that we want to prove A ∨ B from A and also from B. Below, in the place of the type of the conclusion, we can't use put the term h₁.

variable h₁ : A ∨ B

example (h : A) : ??? := or.inl h


So the possible silly question is. How can we use an object (term) in a place expecting a type?

#### Andrew Ashworth (Sep 04 2019 at 12:30):

use a definition?

#### Alexandre Rademaker (Sep 04 2019 at 12:40):

hum, can you ellaborate on that?

#### Reid Barton (Sep 04 2019 at 12:48):

Something like def my_conclusion := A ∨ B

#### Andrew Ashworth (Sep 04 2019 at 12:50):

but also you can't put h1 inside there because those are two different formulas. If I understand you correctly what you actually have is

variables (p q : Prop)
example : p → p ∨ q := λ hp, or.intro_left q hp
example : q → p ∨ q := λ hq, or.intro_right p hq


#### Alexandre Rademaker (Sep 04 2019 at 12:51):

Something like def my_conclusion := A ∨ B

In the code below, nor h₁ or h₂ works in the example:

variables A B : Prop
def h₁ := A ∨ B
variable h₂ : A ∨ B

example (h : A) : ??? := or.inl h


#### Andrew Ashworth (Sep 04 2019 at 12:55):

variables (p q : Prop)
example : p → p ∨ q := λ hp, or.intro_left q hp
example : q → p ∨ q := λ hq, or.intro_right p hq

def p_or_q : Prop := p ∨ q

example : p → p_or_q p q := λ hp, or.inl hp


#### Reid Barton (Sep 04 2019 at 12:55):

It needs to be h₁ A B

#### Alexandre Rademaker (Sep 04 2019 at 12:56):

but also you can't put h1 inside there because those are two different formulas. If I understand you correctly what you actually have is

variables (p q : Prop)
example : p → p ∨ q := λ hp, or.intro_left q hp
example : q → p ∨ q := λ hq, or.intro_right p hq


yes, I don't want to repeat the p ∨ q!

#### Andrew Ashworth (Sep 04 2019 at 12:57):

ahh maybe you want parameters then

section
parameters (p q : Prop)

def p_or_q : Prop := p ∨ q

example (hp : p) : p_or_q := or.inl hp
example (hq : q) : p_or_q := or.inr hq

end


#### Alexandre Rademaker (Sep 04 2019 at 12:59):

TL;DR. Suppose I have an encoding of the hamiltonian cycle of a graph in propositional formulas. See https://www.csie.ntu.edu.tw/~lyuu/complexity/2011/20111018.pdf. An SAT solver can give me one possible path as a truth assignment. I want to use Lean to deduce the model cheking. That is, to show that this assignment is really a model for the formulas. So what I want is to have the formulas declared first and after that introduce a set of theorems showing that all of them can be proved from the AND formula that encodes the truth assignment. Hope the motivation is clear enough.

#### Alexandre Rademaker (Sep 04 2019 at 13:12):

Nice, parameters work. But I need to understand the difference between parameters and variables in a section. I was expecting that declaring the variables with variables {p q : Prop} would also allow me to type only p_or_q instead of p_or_q p q, but that didn't happen. Actually, maybe I didn't yet understood the difference between introducing a variable and introduce a definition. In introducing definitions it says: "declaring constants in the Lean environment is a good way to postulate new objects to experiment with, but most of the time what we really want to do is define objects in Lean and prove things about them."

#### Andrew Ashworth (Sep 04 2019 at 13:19):

parameters vs variables is discussed in chapter 6 of TPIL

Last updated: May 13 2021 at 05:21 UTC