Specializing forall quantifiers in Coq

Question

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.

Answer 1

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)
}.