Lean equivalent to Coq programs?

Stream: Is there code for X?

[Quarrie]

Long story short I am in a situation where I need to convert at will between an inductive type parametrized with a * (b * c) and with (a * b) * c, and thus need to code the Lean equivalent of a Program. Does Lean have a mechanism for this?

[Eric Wieser]

Can you maybe give a #mwe to elaborate a bit more on what you mean?

[Quarrie]

Eric Wieser In Coq, I can prove two non-defeq types to be equal using the Program feature:

Require Import Program.
Require Import Arith.

Parameter Matrix : nat -> nat -> Type.
Parameter Id : forall (n : nat), Matrix n n.

Program Definition id_eq : forall m n, Id (m + n) = Id (n + m) := _.

Next Obligation.
  apply Nat.add_comm.
Defined.

Next Obligation.
  apply Nat.add_comm.
Defined.

Next Obligation.
  unfold id_eq_obligation_1.
  unfold id_eq_obligation_2.
  elim_eq_rect.
  reflexivity.
Defined.

[Quarrie]

Definition coerce_matrix {m n} : Matrix (m + n) (m + n) -> Matrix (n + m) (n + m).
  intros A.
  rewrite Nat.add_comm.
  exact A.
Defined.

Lemma id_eq' : forall m n, Id (m + n) = coerce_matrix (Id (n + m)).

Proof.
  intros.
  unfold coerce_matrix.
  unfold eq_rect_r.
  elim_eq_rect.
  reflexivity.
Qed.

[Quarrie]

(Code here is courtesy of Robert Rand)

[Quarrie]

In Lean, I have run into a similar issue where due to the equal types not being definitionally equal I need to prove them equal and then create an identity associator

[Quarrie]

I have this working definition

import algebra.module.basic
import analysis.inner_product_space.basic
import linear_algebra.bilinear_form
import linear_algebra.tensor_product

namespace inner_product_space

universe u

def tpow (E : Type u) (t : Type u -> Type u -> Type u) : nat -> Type u
| 0 := E -- This is not ideal, but not dealing with the concept of zero is faster for prototyping than doing it idiomatically
| (n + 1) := (t E (tpow n))

variable E : Type u
variable prod : Type u -> Type u -> Type u
reserve postfix `^` : 100000
local notation v`^` := tpow E prod v

class tensor_product_family (R : Type u) (E : Type u) (prod : Type u -> Type u -> Type u) (prod_t : forall (AA BB : nat), AA^ -> BB^ -> (((AA + 1) * (BB + 1)) - 1)^) [semiring R] [add_comm_monoid E] [module R E] :=
  (space_product_associative : forall (a b : nat), ((prod a^ b^) = (((a + 1) * (b + 1)) - 1)^))
  (space_product_generates_add_comm_monoids : forall (a b : nat), (add_comm_monoid (((a + 1) * (b + 1)) - 1)^))

[Quarrie]

And I try to add this line

  (element_product_associative : forall (a b g : nat) (x : a^) (y : b^) (z : g^), ((prod_t _ _ x (prod_t _ _ y z)) = (prod_t _ _ (prod_t _ _ x y) z)))

[Quarrie]

Which predictably throws the following type error

/home/quarrie/Git/mathlib_testing/src/tensor_product.lean:38:115: error: type mismatch at application
  prod_t a ((b + 1) * (g + 1) - 1) x (prod_t b g y z) = prod_t ((a + 1) * (b + 1) - 1) g (prod_t a b x y) z
term
  prod_t ((a + 1) * (b + 1) - 1) g (prod_t a b x y) z
has type
  tpow E prod (((a + 1) * (b + 1) - 1 + 1) * (g + 1) - 1)
but is expected to have type
  tpow E prod ((a + 1) * ((b + 1) * (g + 1) - 1 + 1) - 1)

[Patrick Johnson]

Try == instead of =

[Eric Wieser]

Here's my best attempt at translating that Coq code:

import tactic

section
parameter Matrix : nat -> nat -> Type
parameter Id : Π (n : nat), Matrix n n

lemma id_eq : ∀ m n, Id (m + n) == Id (n + m) :=
begin
  intros m n,
  rw nat.add_comm,
end

def coerce_matrix {m n} : Matrix (m + n) (m + n) → Matrix (n + m) (n + m) :=
begin
  intros A,
  rw nat.add_comm,
  exact A
end

lemma id_eq' : ∀ m n, Id (m + n) = coerce_matrix (Id (n + m)) :=
begin
  intros m n,
  dsimp only [coerce_matrix],
  rw [eq_mpr_eq_cast, eq_comm, cast_eq_iff_heq],
  exact id_eq _ _
end

end

[Eric Wieser]

Note lean doesn't even let me state id_eq with =, because the terms don't have the same type

[Eric Wieser]

Related, you might be interested in #10255 which defines tensor powers as ⨂[R] i : fin n, M (in terms of docs#pi_tensor_product)