terms as types?

Stream: new members

[Alexandre Rademaker]

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]

use a definition?

[Alexandre Rademaker]

hum, can you ellaborate on that?

[Reid Barton]

Something like def my_conclusion := A ∨ B

[Andrew Ashworth]

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]

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]

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]

It needs to be h₁ A B

[Alexandre Rademaker]

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]

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]

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]

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]

parameters vs variables is discussed in chapter 6 of TPIL