## Stream: general

### Topic: Better Implication

#### Nima (Apr 19 2018 at 04:20):

I can write if h:cnd then aa else bb.
Suppose I only want to write something like h:cnd → aa (else branch is true).
Is there anyway to do this without writing if h:cnd then aa else true?
The similar question is for h:cnd ∧ aa.
I rather not use ∀h:cnd, aa, since if I have cnd or its complement in local hypotheses, simp does not simplify.

#### Kenny Lau (Apr 19 2018 at 04:20):

just write cnd -> aa?

#### Nima (Apr 19 2018 at 04:22):

I want to use h in RHS

#### Nima (Apr 19 2018 at 04:30):

Here is an example (please ignore the actual definitions, just the usage),

variable α : Type
def exp (a:α) (h:a0) : a * a = a := sorry -- some function that takes an input and requires something to be true about that input
example (a:α) :  a:α, h:a0  a = exp a h -- for any a in the domain of exp, we have some property

#### Kenny Lau (Apr 19 2018 at 04:31):

the "standard" approach in mathlib is to define the function without assuming the condition, and prove the theorems assuming the condition

#### Kenny Lau (Apr 19 2018 at 04:31):

i.e. don't make the condition one of the arguments to the function

#### Nima (Apr 19 2018 at 04:34):

Not sure that is what I wanted. For example, I can always use if then else, but then one branch is always useless. I was looking for a solution to this problem, not erasing it. ;)

#### Kenny Lau (Apr 19 2018 at 04:35):

I don't recommend using if then else at all

#### Mario Carneiro (Apr 19 2018 at 04:37):

You should use ∀h:cnd, aa in this case

#### Nima (Apr 19 2018 at 04:41):

Well, simp does not handle ∀h:cnd, aa when I have h:cnd in local hypotheses. Right? Any other way, to automatically simplify ∀h:cnd, aa (this will be more serious when the quantification is part of a bigger condition)

specialize

#### Mario Carneiro (Apr 19 2018 at 04:54):

I see. Tell me whether these simp lemmas work in your use-case:

@[simp] theorem forall_prop_of_true {p : Prop} {q : p → Prop} (h : p) : (∀ h' : p, q h') ↔ q h :=
@forall_const (q h) p ⟨h⟩

@[simp] theorem exists_prop_of_true {p : Prop} {q : p → Prop} (h : p) : (∃ h' : p, q h') ↔ q h :=
@exists_const (q h) p ⟨h⟩

@[simp] theorem forall_prop_of_false {p : Prop} {q : p → Prop} (hn : ¬ p) : (∀ h' : p, q h') ↔ true :=
iff_true_intro \$ λ h, hn.elim h

@[simp] theorem exists_prop_of_false {p : Prop} {q : p → Prop} : ¬ p → ¬ (∃ h' : p, q h') :=
mt Exists.fst

#### Mario Carneiro (Apr 19 2018 at 04:57):

But I will remark that this situation is rather rare in mathlib, because we try to avoid partial functions, which tend to make rewriting difficult. From the code you've shown here before, you seem to prefer partial functions

#### Nima (Apr 19 2018 at 05:01):

Thank you, they help.
Did you just wrote them?
Also, the last one does not type check.

#### Mario Carneiro (Apr 19 2018 at 05:08):

Yes I did. For the last one you should have logic.basic imported

#### Nima (Apr 19 2018 at 05:09):

I haven't done anything about code generation. But what I have in mind is a type that take parameters and has different fields based on values of those parameters. In C++, I can easily use template to have those fields defined based on the input template arguments. In Lean, I am trying to have the same effect, by making sure that every time I am reading a field, it is defined.

structure constraint
(α : Type*)
(trvk : triviality_kind)
(dirk : direction_kind )
(strk : strictness_kind)
:=
cnstr ::
(tri : trvk = triviality_kind.kdyn  triviality)
(str : strk = strictness_kind.kdyn  strictness)
(bnd : trvk  triviality_kind.ktrv  α         )

#### Mario Carneiro (Apr 19 2018 at 05:11):

(I'm assuming the reason it doesn't typecheck is because it says Exists.fst can't be found; that's a hint.)

#### Mario Carneiro (Apr 19 2018 at 05:13):

I would suggest using an inductive type to encode these constraints

#### Mario Carneiro (Apr 19 2018 at 05:15):

I think it will be easier for you to return a default value when you can, and an option when there is no reasonable default, to totalize your functions. If you are going for efficiency, this won't achieve it anyway due to thunk generation

#### Mario Carneiro (Apr 19 2018 at 05:16):

Could you link to your files where you define these triviality_kind etc? Let me make a mockup

#### Nima (Apr 19 2018 at 05:19):

I used that first, but it has its own problem.
For example, suppose I have two constraints and I want to add them.
But not only I want to define addition for constraints with the same type parameters, but also in case the result cannot be represented by a constraint, I want to return a smallest representable constraint that is of the right type. If I push everything inside one inductive type, then I have to put extra condition on the signature of addition (or I don't know how else I can do it).
https://github.com/nima-roohi/lets-learn-some-lean

#### Mario Carneiro (Apr 19 2018 at 05:24):

What does adding constraints mean here? If I understand your model correctly, you want to be able to represent the sets true, {x | x R a}, and {x | a R x} where R is <= or <. Does adding the sets mean all pointwise additions, i.e. {x + y | x \in c1, y \in c2}, or the intersection / union of constraints or something else?

#### Nima (Apr 19 2018 at 05:26):

addition is just an example. You can assume pointwise addition as you defined.
If α is, for example, float then even addition of two constraints cannot always be represented by a constraint.

#### Nima (Apr 19 2018 at 05:31):

Is there anyway I can change this notation so the example will work?

notation  c:h → hh := if c:h then hh else true
example : (h : 1>2)  1>2 := sorry

#### Mario Carneiro (Apr 19 2018 at 05:35):

Here's more or less what I'm thinking:

import algebra.ordered_group

inductive constraint (α : Type*)
| triv {} : constraint
| le : α → constraint
| lt : α → constraint
| ge : α → constraint
| gt : α → constraint

namespace constraint

def is_trivial {α} : constraint α → bool
| constraint.triv := tt
| _ := ff

def get_bound {α} : constraint α → option α
| constraint.triv := none
| (constraint.le a) := some a
| (constraint.lt a) := some a
| (constraint.ge a) := some a
| (constraint.gt a) := some a
--add others to taste, but you shouldn't need them

protected def mem {α} [preorder α] (x : α) : constraint α → Prop
| constraint.triv := true
| (constraint.le a) := a ≤ x
| (constraint.lt a) := a < x
| (constraint.ge a) := x ≤ a
| (constraint.gt a) := x < a

instance {α} [preorder α] : has_mem α (constraint α) := ⟨constraint.mem⟩

protected def add {α} [ordered_comm_group α] : constraint α → constraint α → constraint α
| constraint.triv c2 := c2
| c1 constraint.triv := c1
| (constraint.le a) (constraint.le b) := constraint.le (a + b)
| (constraint.le a) (constraint.lt b) := constraint.lt (a + b)
| (constraint.lt a) (constraint.le b) := constraint.lt (a + b)
| (constraint.lt a) (constraint.lt b) := constraint.lt (a + b)
| (constraint.ge a) (constraint.ge b) := constraint.ge (a + b)
| (constraint.ge a) (constraint.gt b) := constraint.gt (a + b)
| (constraint.gt a) (constraint.ge b) := constraint.gt (a + b)
| (constraint.gt a) (constraint.gt b) := constraint.gt (a + b)
| _ _ := constraint.triv

end constraint

#### Mario Carneiro (Apr 19 2018 at 05:37):

You can't define the arrow and colon as notations; they are reserved for function types

#### Nima (Apr 19 2018 at 05:43):

I see what you mean by making a function total.
May be that makes things easier.
But I am not sure about performance of the result code.
Also, in your definition you only have one le, but I have two of them (dynamic vs static). So if every time I have to write all the cases, that might be a problem itself.

#### Mario Carneiro (Apr 19 2018 at 05:58):

Okay, version 2:

import algebra.ordered_group

inductive direction | lower | upper

inductive constraint (α : Type*)
| triv {} : constraint
| mk (dir : direction) (strict : bool) (dynamic : bool) (bound : α) : constraint

namespace constraint
open direction

def is_trivial {α} : constraint α → bool
| triv := tt
| _ := ff

def get_bound {α} : constraint α → option α
| triv := none
| (mk a s d b) := some b

protected def mem {α} [preorder α] (x : α) : constraint α → Prop
| triv := true
| (mk lower ff d a) := a ≤ x
| (mk lower tt d a) := a < x
| (mk upper ff d a) := x ≤ a
| (mk upper tt d a) := x < a

instance {α} [preorder α] : has_mem α (constraint α) := ⟨constraint.mem⟩

protected def add {α} [ordered_comm_group α] : constraint α → constraint α → constraint α
| (mk lower s1 d1 a) (mk lower s2 d2 b) := mk lower (s1 || s2) (d1 || d2) (a + b)
| (mk upper s1 d1 a) (mk upper s2 d2 b) := mk upper (s1 || s2) (d1 || d2) (a + b)
| _ _ := constraint.triv

end constraint

#### Nima (Apr 19 2018 at 06:09):

Thank you.
I guess the biggest difference between what you wrote and what I have is that, assuming we are defining the same concept, in my definition when dynamic is ff then there is no field named strict (at least intuitively). If I preserve that restriction throughout my definition, (I hope) that transforming these into a code would be easier, at least when I do it manually!!

#### Mario Carneiro (Apr 19 2018 at 06:26):

I'm making up stuff as I go along re: the actual semantics, but I assume it looks something like this:

import algebra.ordered_group

inductive direction | lower | upper
inductive strictness | stt | nst | dyn

namespace strictness

def is_strict : strictness → bool
| stt := tt
| _ := ff

def join : strictness → strictness → strictness
| dyn _ := dyn
| _ dyn := dyn
| stt _ := stt
| _ stt := stt
| _ _ := nst

end strictness

inductive constraint (α : Type*)
| triv {} : constraint
| mk (dir : direction) (strict : strictness) (bound : α) : constraint

namespace constraint
open direction

def is_trivial {α} : constraint α → bool
| triv := tt
| _ := ff

def get_bound {α} : constraint α → option α
| triv := none
| (mk a s b) := some b

protected def mem {α} [preorder α] (x : α) : constraint α → Prop
| triv := true
| (mk lower s a) := if s.is_strict then a < x else a ≤ x
| (mk upper s a) := if s.is_strict then x < a else x ≤ a

instance {α} [preorder α] : has_mem α (constraint α) := ⟨constraint.mem⟩

protected def add {α} [ordered_comm_group α] : constraint α → constraint α → constraint α
| (mk lower s1 a) (mk lower s2 b) := mk lower (s1.join s2) (a + b)
| (mk upper s1 a) (mk upper s2 b) := mk upper (s1.join s2) (a + b)
| _ _ := constraint.triv