# Specializing forall quantifiers in Coq

I have an inductively defined type of expressions:

Inductive Expr {v:Type} : Type :=
| ExprVar (var:v)
| ExprZero
| ExprOne
| ExprPlus (e1 e2 : Expr)
| ExprTimes (e1 e2 : Expr).


Along with a Semiring is a typeclass:

Class Semiring d : Type :=
{
Zero : d;
One : d;
Add : d -> d -> d;
Mul : d -> d -> d;
AddId : forall a : d, Add a Zero = a;
AddComm : forall a b : d, Add a b = Add b a;
AddAssoc : forall a b c : d, Add a (Add b c) = Add (Add a b) c;
MulId : forall a : d, Mul a One = a;
MulComm : forall a b : d, Mul a b = Mul b a;
MulAssoc : forall a b c : d, Mul a (Mul b c) = Mul (Mul a b) c;
MulDistr : forall a b c : d, Mul a (Add b c) = Add (Mul a b) (Mul a c)
}.


And an inductively defined structure preserving property of functions between semirings, defined with a universal quantifier over elements x and y of the semiring:

Inductive Semi_Hom {A B : Type} {sra:Semiring A} {srb:Semiring B} (h : A -> B) : Prop :=
| h_hom : forall (x y:A),
h Zero = Zero ->
h One = One ->
h (Add x y) = Add (h x) (h y) ->
h (Mul x y) = Mul (h x) (h y) -> Semi_Hom h.


I would like to prove the equivalence of two evaluation functions given said property:

Fixpoint evalExpr' {v : Type}
{srd:Semiring v}
(e : @Expr v) : v :=
match e with
| ExprVar x => x
| ExprZero => Zero
| ExprOne => One
| ExprPlus e1 e2 => Add (evalExpr' e1) (evalExpr' e2)
| ExprTimes e1 e2 => Mul (evalExpr' e1) (evalExpr' e2)
end.

Fixpoint evalExpr {v d : Type}
{srd:Semiring d}
(var : v -> d)
(e : @Expr v) : d :=
match e with
| ExprVar x => var x
| ExprZero => Zero
| ExprOne => One
| ExprPlus e1 e2 => Add (evalExpr var e1) (evalExpr var e2)
| ExprTimes e1 e2 => Mul (evalExpr var e1) (evalExpr var e2)
end.

Theorem expr_eval_equivalence :
forall {v d:Type} {srv:Semiring v} {srd:Semiring d},
forall (var:v -> d) (e:@Expr v),
Semi_Hom var -> var (evalExpr' e) = evalExpr var e.
Proof.
intros v d srv srd var e shv.
destruct shv as [x y var_preserves_zero var_preserves_one
var_preserves_add var_preserves_mul].
induction e as [ | | | e1 IHe1 e2 IHe2 | e1 IHe1 e2 IHe2].
- reflexivity.
- simpl. apply var_preserves_zero.
- simpl. apply var_preserves_one.
- simpl. rewrite <- IHe1. rewrite <- IHe2.
(* stuck! *)


I am left with the following proof state:

  v : Type
d : Type
srv : Semiring v
srd : Semiring d
var : v -> d
e1, e2 : Expr
x, y : v
var_preserves_zero : var Zero = Zero
var_preserves_one : var One = One
var_preserves_add : var (Add x y) = Add (var x) (var y)
var_preserves_mul : var (Mul x y) = Mul (var x) (var y)
IHe1 : var (evalExpr' e1) = evalExpr var e1
IHe2 : var (evalExpr' e2) = evalExpr var e2
============================
var (Add (evalExpr' e1) (evalExpr' e2))
= Add (var (evalExpr' e1)) (var (evalExpr' e2))


Now I would really like to specialize the x and y variables to evalExpr' e1 and evalExpr' e2 for them to be useful; how would I go about this? I tried shifting the variables back into the goal with generalize dependent,

  v : Type
d : Type
srv : Semiring v
srd : Semiring d
var : v -> d
e1, e2 : Expr
var_preserves_zero : var Zero = Zero
var_preserves_one : var One = One
IHe1 : var (evalExpr' e1) = evalExpr var e1
IHe2 : var (evalExpr' e2) = evalExpr var e2
============================
forall y x : v,
var (Add x y) = Add (var x) (var y) ->
var (Mul x y) = Mul (var x) (var y) ->
var (Add (evalExpr' e1) (evalExpr' e2))
= Add (var (evalExpr' e1)) (var (evalExpr' e2))


but I cannot find a tactic that would let me introduce these with the right instance. I could've sworn I saw a mechanism like that somewhere in Software Foundations but I cannot find it now.

• Can you give us enough context to be able to execute your code? In particular, the definition of Semiring and the typeclasses/notations/canonical structures setup to be able to go through your definition of Semihom? Sep 1 at 9:41
• Of course, I will put in some more context, sorry. I'm not sure how to make it a little more concise unfortunately. Sep 1 at 15:05

## 1 Answer

The issue comes from your definition of semi-ring morphism. It does not say that a semi-ring homomorphism preserves addition, but rather that there exists some unspecified x,y for which addition is preserved. You can see that in the following:

Require Import Nat Lia.

#[global] Instance semi_nat : Semiring nat.
Proof.
exists 0 1 add mul.
all: intros ; lia.
Defined.

Definition h (n : nat) : nat :=
match n with
| 0 => 0
| S _ => 1
end.

Lemma weird : Semi_Hom h.
Proof.
exists 0 0.
all: reflexivity.
Qed.


but of course h is not a semiring morphism…

The definition you want for semi-ring morphism is probably the following:

Class Semi_Hom {A B : Type} {sra:Semiring A} {srb:Semiring B} (h : A -> B) : Prop :=
{
zero_hom : h Zero = Zero ;
one_hom : h One = One ;
add_hom x y : h (Add x y) = Add (h x) (h y) ;
mul_hom x y : h (Mul x y) = Mul (h x) (h y)
}.

• This solves my usecase, thank you very much! Maybe I'm taking forall a little too literally here Sep 1 at 16:08
• You just have to be careful how you parenthesize: forall x y, Add (h x) (h y) = h (Add x y) -> Semi_hom h is not the same as (forall x y, Add (h x) (h y) = h (Add x y)) -> Semi_hom h. Sep 1 at 16:22
• That is a very useful tip actually, thank you Sep 1 at 16:37