Coq: Defining a special function

Question

I want to define a function f w/ 2 explicit arguments. The types of the arguments and value of f are applications of some g. Suppose the arguments' types are g x y and g z w. The tricky part is that f's value must depend on the unifiability of x and z. Below is a naive attempt at defining f that fails. How should I tackle this?

Inductive A := a | a0 | fa.
Inductive B := b | b0.
Parameter C: Type.
Parameter g: A -> B -> C.
Parameter CT:> C -> Type.
Parameter gab: g a b.
Parameter ga0b: g a0 b.

Definition f {x y z w}(n: g x y)(m: g z w) :=
ltac:(match x with z => exact (g z b) | _  => exact (g fa b) end).

Compute f gab ga0b. (*= g fa b: C*)
Compute f gab gab. (*! = g fa b: C !*)

Answer 1

f's value must depend on the unifiability of x and z

It is impossible to write such a definition. Suppose you could write a function that could tell whether or not two natural numbers unified, call it unify_nat : nat -> nat -> bool. Consider now the functions

F := fun x y : nat => if unify_nat (x + y) (y + x) then True else False
G := fun x y : nat => if unify_nat (x + y) (x + y) then True else False

We can prove, because addition is commutative, that forall x y, F x y = G x y. But then unify_nat (x + y) (y + x) must return true, even though x + y and y + x do not unify.

---

There are two things you can do: (1) you can ask not if the terms unify, but if they are propositionally equal; and (2) you can write a notation, or an alias, which is like syntactic sugar for a definition.

1.

The command Scheme Equality will generate an equality decision function for most inductive types:

Scheme Equality for A.
Definition f {x y z w}(n: g x y)(m: g z w) :=
  if A_beq x z then g z b else g fa b.

Compute f gab ga0b. (*= g fa b: C*)
Compute f gab gab. (*= g a b: C*)

2.

We can create evars with open_constr:(_) and use unification to infer the types of n and m:

Ltac f_tac n m :=
  let x := open_constr:(_) in
  let y := open_constr:(_) in
  let z := open_constr:(_) in
  let w := open_constr:(_) in
  let n := constr:(n : g x y) in
  let m := constr:(m : g z w) in
  match x with z => exact (g z b) | _  => exact (g fa b) end.
Notation f n m := (ltac:(f_tac n m)) (only parsing).

Compute f gab ga0b. (*= g fa b: C*)
Compute f gab gab. (*= g a b: C*)