How to prove equivalence of values

Stream: new members

[Jonathan Lacombe]

What is the approach of proving equivalence of values of inductive types? The Eq type only has propIntro which doesn't help here. What sort of tactics could I use?

In the example below, I assume the helper neg_neg function needs to be used but not sure how to use it.

inductive Value where
  | unit
  | neg (v: Value)

def Value.neg_neg (v: Value) :=
  match v with
  | neg (neg x) => x
  | other => other

theorem Value.value_eq_neg_neg {v: Value}: v = neg (neg v) := by
  sorry

[Etienne Marion]

I can’t see why your theorem is true. It looks like what you are stating is equivalent to saying that succ (succ 0) = 0.

[Ruben Van de Velde]

Yeah, it's not true

[Ruben Van de Velde]

Value.neg_neg confused me, but it's just a function. It doesn't change anything about the equality

[Ruben Van de Velde]

Distinct constructors of an inductive type create distinct values by definition

[Yaël Dillies]

I think Jonathan wants to prove

theorem Value.value_eq_neg_neg {v: Value}: v.neg_neg = (neg (neg v)).neg_neg := rfl

[Jonathan Lacombe]

Etienne Marion said:

I can’t see why your theorem is true. It looks like what you are stating is equivalent to saying that succ (succ 0) = 0.

I'm trying to say that neg (neg n) = n or -(-n) = n. I guess since this is a new inductive type, what I am really asking is how do I introduce this equivalence? And maybe then I can prove it is true?

I am really new to this theorem proving stuff so I don't even know if that makes sense. But I would assume this can be done somehow since in the standard library there is Int.neg_neg which can prove the same thing for actual integers.

[Jonathan Lacombe]

Ruben Van de Velde said:

Distinct constructors of an inductive type create distinct values by definition

The inductive type of Int defined in Lean looks like this:

inductive Int : Type where
  | ofNat   : Nat → Int
  | negSucc : Nat → Int

Here it doesn't seem like there is really any information about what is "negative". But somehow they introduce this concept and are able to prove similar propositions. I guess what I am asking is how is this done?

[Jonathan Lacombe]

Yaël Dillies said:

I think Jonathan wants to prove

theorem Value.value_eq_neg_neg {v: Value}: v.neg_neg = (neg (neg v)).neg_neg := rfl

I think that would work too. But if I am able to prove that, I should also be able to prove the one I mentioned above right?

[Etienne Marion]

Jonathan Lacombe said:

Here it doesn't seem like there is really any information about what is "negative". But somehow they introduce this concept and are able to prove similar propositions. I guess what I am asking is how is this done?

In Mathlib, the way it is done is by defining docs#Int.neg. This is a function which sends an integer to what you would expect to be its negative version. You should do something similar in your case: define a function Value.neg' (v : Value) := unit => neg unit | neg v => v, and then prove

theorem neg'_neg' (v : Value) : v.neg'.neg' = v := sorry

[Jonathan Lacombe]

This seems to be what I am looking for. Thanks for this, I will try this out.

[Etienne Marion]

In fact the theorem I wrote down is not true: unit.neg.neg.neg'.neg' = unit whereas it should be equal to unit.neg.neg.

[Etienne Marion]

In fact the type you defined is really the same as Nat. And the function I defined is the one sending 0 to 1 and any other integer to its predecessor, so it's not an involution. Maybe the structure of your type is not the one you are looking for?

[Jonathan Lacombe]

Etienne Marion said:

In fact the type you defined is really the same as Nat. And the function I defined is the one sending 0 to 1 and any other integer to its predecessor, so it's not an involution. Maybe the structure of your type is not the one you are looking for?

Yeah, I think you're right. And this is probably what @Ruben Van de Velde was saying earlier. I was trying to prove equivalence of two structures that are different. I really am beginning to understand a lot from this. The reason double negation "works" for the Int type is because neg just sends ofNat(n) to negSucc and vice-versa.

The way I am describing "negation" would make sense with a structure like below (which checks out):

inductive Boolean where
  | T
  | F

def Boolean.not (b: Boolean) :=
  match b with
  | T => F
  | F => T

theorem Boolean.not_not (b: Boolean): b.not.not = b := by
  induction b <;> rfl

However, I can't just change the structure because what I really am trying to do is create a type that defines "operations" that can be done on another type. I wanted to represent computational operations (ex: C math functions sin, floor, pow, etc) and then find "similar" operations that I can replace with another. Also, I wanted to do this without defining the type that is being operated on.

I don't have a background in mathematics or proofs and I know this might sound unusual or even unsound, especially considering that these operations are not really replaceable since resulting values may actually turn out to be different. But this doesn't need to have a rigorous proof, it's just an experiment to see if I can find some small optimizations. Like finding a sin(pi) and replacing with 0.

Anyway, thanks for your help. I am starting to know what direction I should take.

And in case you're wondering, considering the context above, I will look into proving statements like this:

inductive BooleanOp
  | identity
  | and (a: BooleanOp) (b: BooleanOp)
  | or (a: BooleanOp) (b: BooleanOp)
  | not (b: BooleanOp)

def reducible (a: BooleanOp) (b: BooleanOp): Bool :=
  sorry

theorem BooleanOp.not_not (b: BooleanOp): reducible b.not.not b := by
  sorry

[Ruben Van de Velde]

Right, in this context you can work with a kind of equivalence relation, but not equality, because the equality is equality of terms, not "values"

[Ruben Van de Velde]

Once you have that relation, you can create a quotient type - but perhaps try playing with the relation first

[Etienne Marion]

That looks interesting, have fun! And don’t hesitate to open a new topic if you have other questions