# Zulip Chat Archive

## 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 isvariables (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