conditional definition

Stream: new members

[Raphael Appenzeller]

I would like to define something by cases. How do I do this and how do I resolve it when proving things about it?
In the following example I am trying to define a distance function on a disjoint union of three intervals. MWE:

class my_metric_space (X:Type*) :=
(my_dist : X → X → ℝ  )
(my_dist_nonneg := ∀ x y : X, my_dist x y ≥ 0)

def counterexample_carrier := {t : ℝ   | 0 ≤ t ∧ t ≤ 1} × {i : ℕ | i=1 ∨ i=2 ∨ i=3 }

instance counterexample : my_metric_space counterexample_carrier :=
{
    my_dist := λ x y ,  if x.2 = y.2 then |x.1-y.1| else 1 - (x.1 + y.1),
    my_dist_nonneg := by sorry,
}

[Yaël Dillies]

You can use split_ifs to case on an if then else. Else I'm not sure what you're asking about because this looks good!

[Yaël Dillies]

Just note that if p then ... else ... requires p to be decidable. So here you will need to provide decidable_eq {i : ℕ | i=1 ∨ i=2 ∨ i=3 } (you can cheat and use docs#classical.dec_eq)... or just use fin 3 instead.

[Raphael Appenzeller]

Thanks! split_ifs was what I was searching (and I was not sure that my if then else-syntax is correct.

[Yaël Dillies]

You will also find docs#if_pos and docs#if_neg useful.

[Raphael Appenzeller]

I have created this example as above and would like to now prove things about it. How do I reference it correctly. (The follownig is referencing it incorrectly:

import data.real.basic

class my_metric_space (X:Type*) :=
(my_dist : X → X → ℝ  )
(my_dist_nonneg : ∀ x y : X, my_dist x y ≥ 0)

def counterexample_carrier := {t : ℝ   | 0 ≤ t ∧ t ≤ 1} × fin 3 -- {i : ℕ | i=0 ∨ i=1 ∨ i=2 }

noncomputable instance counterexample : my_metric_space counterexample_carrier :=
{
    my_dist := λ x y ,  if x.2 = y.2 then |x.1-y.1| else 2 - (x.1 + y.1),
    my_dist_nonneg := begin
       sorry,
    end,
}

def property (X : Type*) [my_metric_space X] :  ∃ p q : X , my_metric_space.my_dist p q ≠ 0

lemma lem : property counterexample :=
begin
  sorry,
end

[Mario Carneiro]

the theorem looks false: (1, 0) and (1, 1) are distance -1 apart

[Mario Carneiro]

(also your comment is incorrect - fin 3 is {0, 1, 2} not {1, 2, 3})

[Raphael Appenzeller]

Yes, thank you. i think the MWE is now actually correct and you can play around with it if you want.
I mainly wonder how I use counterexample in a lemma.

[Mario Carneiro]

you normally shouldn't reference instances directly by name

[Mario Carneiro]

so the theorem should be property counterexample_carrier

[Raphael Appenzeller]

Unfortunately this does not work either

lemma lem : property counterexample_carrier :=
begin
  sorry,
end

I get the error:

type expected at
  property counterexample_carrier
term has type
  ∃ (p q : counterexample_carrier), my_metric_space.my_dist p q ≠ 0

[Mario Carneiro]

That's because you have a syntax error at def property, you probably want := not :

[Raphael Appenzeller]

Omg, yes that solved it. Thanks for your help!

[Raphael Appenzeller]

I have anothe question about the if then else or ite-construction. Is there a way to explicitly reference the hypothesis inside the then or else branch? For example I can do the following:

if h : x.2 = y.2 then (statement using h) else (statement using a proof for not h)

But how do I get a proof for \not x.2 = y.2 in the else-branch? I cannot do \not h.

[Alex J. Best]

In both branches the hypothesis will be called h, it will just have a different type in the else branch

[Raphael Appenzeller]

Hmm, yes. In the proof it will get a default name which is h (or h_1 if h is already taken), but is there a way to already access this hypothesis already in the ite-statement?

[Raphael Appenzeller]

As an example, I might want to use the above counterexample to define a map as follows:

def map  : {t : ℝ  | 0 ≤ t ∧ t ≤ 2 } → counterexample_carrier :=
   λ t , if (t:ℝ) ≤ 1 then (t + 1 , 1) else ( 2 - t  , 2)

But the problem is that Lean wants to be sure that t+1 (or (t:\R)+1) is inside the interval [0,2]. To give it that information my idea would be to do the following:

[Mario Carneiro]

I guess you want if t <= 1

[Raphael Appenzeller]

I would use a helper lemma helper to give this info to Lean. But for the proof of the Lemma I need to kknow the conditions of the if. I don't know how to access that. (or whether it is even possible)

class my_metric_space (X:Type*) :=
(my_dist : X → X → ℝ  )
(my_dist_nonneg : ∀ x y : X, my_dist x y ≥ 0)

def counterexample_carrier := {t : ℝ   | 0 ≤ t ∧ t ≤ 1} × fin 3 -- {i : ℕ | i=0 ∨ i=1 ∨ i=2 }

noncomputable instance counterexample  : my_metric_space (counterexample_carrier ):=
{
    my_dist := λ x y ,  if x.2 = y.2 then |x.1-y.1| else 2  - (x.1 + y.1),
    my_dist_nonneg := by sorry,
}

lemma helper (t:ℝ ) (h : t ≤ 2) : 0 ≤ t + 1 ∧ t ≤ 2 := by sorry,

def map  : {t : ℝ  | 0 ≤ t ∧ t ≤ 2 } → counterexample_carrier :=
   λ t , if (t:ℝ) ≤ 1 then (⟨ t + 1 , helper (t:ℝ) h⟩  , 1) else ( ⟨ 2 - t , _ ⟩   , 2)

[Junyan Xu]

You need to write if h : (t:ℝ) ≤ 1

[Junyan Xu]

If you write h : Lean will use docs#dite where you have access to h, otherwise it uses docs#ite which has no dependency on h.

[Raphael Appenzeller]

Ok, this way I might get h in the then-part. But I would be able to use h in the else-part, right?

[Mario Carneiro]

You wrote it already:

if h : x.2 = y.2 then (statement using h) else (statement using a proof for not h)

[Mario Carneiro]

in the else branch you have access to h : x.2 ≠ y.2

[Raphael Appenzeller]

Oh, ok. Yes this works. Thanks! Here is how it looks now:

lemma helper (t:ℝ ) (h : t ≤ 2) : t+1 ∈ {s : ℝ | 0 ≤ s ∧ s ≤ 1} := by sorry
lemma helper2 (t:ℝ ) (h : ¬ (t ≤ 2) ) : 2 -t ∈ {s : ℝ | 0 ≤ s ∧ s ≤ 1} := by sorry
noncomputable def map : {t : ℝ  | 0 ≤ t ∧ t ≤ 2 } → counterexample_carrier :=
   λ t , if h : (t:ℝ) ≤ 2 then (⟨ t + 1 , helper (t:ℝ) h⟩  , 1) else ( ⟨ 2 - t , helper2 (t:ℝ) h ⟩   , 2)

[Mario Carneiro]

you should try to state lemmas that are provable though

[Mario Carneiro]

Neither inequality of 0 <= t+1 <= 1 follows from t <= 2