0
$\begingroup$

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.

$\endgroup$
2
  • $\begingroup$ 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? $\endgroup$ Commented Sep 1, 2023 at 9:41
  • $\begingroup$ Of course, I will put in some more context, sorry. I'm not sure how to make it a little more concise unfortunately. $\endgroup$ Commented Sep 1, 2023 at 15:05

1 Answer 1

2
$\begingroup$

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)
}.
$\endgroup$
3
  • $\begingroup$ This solves my usecase, thank you very much! Maybe I'm taking forall a little too literally here $\endgroup$ Commented Sep 1, 2023 at 16:08
  • 1
    $\begingroup$ 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. $\endgroup$ Commented Sep 1, 2023 at 16:22
  • $\begingroup$ That is a very useful tip actually, thank you $\endgroup$ Commented Sep 1, 2023 at 16:37

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.