Can morte automagically prove that addition commutes?

[ChristopherKing42]

Quick question, would morte be able to prove that addition is commutative?

For example, if you define natural numbers as a recursive type and addition on it, would morte be able to prove that \x -> \y -> x+y is the same as \x -> \y -> y+x. What about if its defined co-recursively?

In general, if two terms have the same semantics, is morte guaranteed to be able to proof them equal (I know it was able to prove the map fusion laws, for example)?

(I would test this myself, but I don't know enough morte to do it.)

[Gabriella439]

No, morte cannot prove commutativity. The best morte can do that I know is to prove associativity.

You can test this yourself by using this program:

(   \(Nat : *)
->  \(Succ : Nat -> Nat)
->  \(Zero : Nat)
->  \((+) : Nat -> Nat -> Nat)
->  \(x : Nat) -> \(y : Nat) -> (+) x y
)

(forall (Nat : *) -> forall (Succ : Nat -> Nat) -> forall (Zero : Nat) -> Nat)

(   \(n : forall (Nat : *) -> forall (Suc : Nat -> Nat) -> forall (Zero : Nat) -> Nat)
->  \(Nat : *)
->  \(Succ : Nat -> Nat)
->  \(Zero : Nat)
->  Succ (n Nat Succ Zero)
)

(   \(Nat : *)
->  \(Succ : Nat -> Nat)
->  \(Zero : Nat)
->  Zero
)

(   \(m : forall (Nat : *) -> forall (Suc : Nat -> Nat) -> forall (Zero : Nat) -> Nat)
->  \(n : forall (Nat : *) -> forall (Suc : Nat -> Nat) -> forall (Zero : Nat) -> Nat)
->  \(Nat : *)
->  \(Succ : Nat -> Nat)
->  \(Zero : Nat)
->  m Nat Succ (n Nat Succ Zero)
)

Same result for the coinductive encoding of natural numbers.

[ChristopherKing42]

Associativity is cool. Is that for both induction and coinduction?

[Gabriella439]

First off, I want to caution that associativity detection only works if you encode addition in the right way. For example, I believe if you define addition as \(m : #Nat ) -> \(n : #Nat ) -> n #Nat #Succ m then the program no longer type-checks. So even in the case of induction you still have to be careful to encode things correctly. There is actually a pretty simple trick to get this right, but I don't know what the name for it is. You just have to explicitly bind every constructor in the final result and then morte will do "the right thing".

For coinduction, definitely not. morte can only prove that terms are equal up to observation (i.e. bisimulation). See my comment here: https://github.com/Gabriel439/Haskell-Morte-Library/issues/30#issuecomment-200919045

[Gabriella439]

I will also mark this closed since I believe the original question was answered, but reopen if you have additional questions