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