## Stream: Coq users

### Topic: ✔ question about eqv to eq

#### yicx (Oct 26 2022 at 00:29):

Hello everyone,

I have developed a xor eqvalence relationships:

================================================
From Coq Require Import String.

Definition var := string.

Inductive term: Type :=
| C : nat -> term
| V : var -> term
| Oplus : term -> term -> term.
Notation "x +' y" := (Oplus x y) (at level 50, left associativity).
Definition T0:term:= C 0.
Reserved Notation "x == y" (at level 70).

Inductive eqv : term -> term -> Prop :=
| eqvA: forall x y z, (x +' y) +' z == x +' (y +' z)
| eqvC: forall x y, x +' y == y +' x
| eqvU: forall x, T0 +' x == x
| eqvN: forall x, x +' x == T0

| eqv_ref: forall x, x == x
| eqv_sym: forall x y, x == y -> y == x
| eqv_trans: forall x y z, x == y -> y == z -> x == z

| Oplus_compat : forall x x' , x == x' -> forall y y' ,
y == y' -> x +' y == x' +' y'
where "x == y" := (eqv x y).
================================================

And right now I really want to prove the following lemma which I theoriotically believe it is correct:

================================================
Lemma test: forall (n:nat),
C n == C 1 -> n = 1.
Proof.
================================================

But I don't know how,
Can anyone gives me some advice on how to proceed?
Or if something went wrong can anyone tell me where went wrong?

Many Thanks!

#### James Wood (Oct 26 2022 at 09:47):

This needs some ingenuity. My intuition would be to give a somewhat normal form to terms as lists of non-zero constants and variables, and then show that for any term equal to a non-zero constant, its somewhat normal form is a singleton of that constant. Then you've reduced a _ == _ expression to a _ = _ expression, which will be a lot easier to work with.

#### James Wood (Oct 26 2022 at 10:01):

Something like:

Definition nf := list (nat + var).
Definition norm : term -> nf.
Lemma norm_C_is_singleton {n t} : t == C (S n) -> norm t = [inl (S n)].
(* By induction on the equivalence *)


I can't remember how to deal with commutativity and transitivity. I think before I've tended to give the algebraic laws as one inductive relation, then take the smallest equivalence relation on that in a more step-by-step way using Rstar.

#### Meven Lennon-Bertrand (Oct 26 2022 at 10:25):

I think things are even worse: not only do you have to deal with associativity + commutativity, there is also the nasty eqvN which, if it is not a typo, means that your normal forms should not be multisets of base cases (constants/variables), but the free $\mathbb{Z}/2\mathbb{Z}$ ring over those. Not only is such quotient, just like multisets, something which is not easily representable in Coq, but although we have some reasonable support for AC/sets, afaik this would have to be done by hand.

#### Meven Lennon-Bertrand (Oct 26 2022 at 10:30):

But I agree that the best solution I can think of is the one outlined by James: define a setoid of normal forms (lists of base cases, modulo associativity, commutativity, and cancellation of pairs), a normalization function to that set, show that it is proper (ie that expressions related by == map to related normal forms), and finally prove that if C m and C n are related normal forms, then m = n. But this is by no means easy!

#### Meven Lennon-Bertrand (Oct 26 2022 at 10:34):

If you remove eqvN, though, there is a much easier solution: instead of interpretation to "normal forms", you can interpret your expressions as integers, show that this interpretation is proper, and use that to conclude easily:

From Coq Require Import String Lia.

Definition var := string.

Inductive term: Type :=
| C : nat -> term
| V : var -> term
| Oplus : term -> term -> term.
Notation "x +' y" := (Oplus x y) (at level 50, left associativity).
Definition T0:term:= C 0.
Reserved Notation "x == y" (at level 70).

Inductive eqv : term -> term -> Prop :=
| eqvA: forall x y z, (x +' y) +' z == x +' (y +' z)
| eqvC: forall x y, x +' y == y +' x
| eqvU: forall x, T0 +' x == x
(*| eqvN: forall x, x +' x == T0*)

| eqv_ref: forall x, x == x
| eqv_sym: forall x y, x == y -> y == x
| eqv_trans: forall x y z, x == y -> y == z -> x == z

| Oplus_compat : forall x x' , x == x' -> forall y y' ,
y == y' -> x +' y == x' +' y'
where "x == y" := (eqv x y).

Fixpoint eval (f : var -> nat) (t : term) : nat :=
match t with
| C n => n
| V v => f v
| x +' y => (eval f x) + (eval f y)
end.

Lemma eval_proper f t u : t == u -> eval f t = eval f u.
Proof.
intros H.
induction H.
all: cbn.
all: lia.
Qed.

Goal forall n, C n == C 1 -> n = 1.
intros n e.
apply (eval_proper (fun _ => 0) _ _ e).
Qed.


#### yicx (Oct 26 2022 at 21:07):

I am goting to try to do something to reduce every term down to normal form.

#### Gaëtan Gilbert (Oct 26 2022 at 21:24):

no need for a full normalizer, you can do a xor count

Fixpoint contains n t :=
match t with
| C n' => Nat.eqb n n'
| V _ => false
| x +' y => xorb (contains n x) (contains n y)
end.

Lemma eqv_contains n (Hn:Nat.eqb n 0 = false) x y : x == y -> contains n x = contains n y.
Proof.
induction 1;simpl.
- apply Bool.xorb_assoc_reverse.
- apply Bool.xorb_comm.
- rewrite Hn;apply Bool.xorb_false_l.
- rewrite Hn;apply Bool.xorb_nilpotent.
- reflexivity.
- symmetry;assumption.
- transitivity (contains n y);assumption.
- congruence.
Qed.

(* "simpl in H" reduces a bit too much without this *)
Arguments Nat.eqb : simpl nomatch.

Goal forall n, C n == C 1 -> n = 1.
Proof.
intros n e.
pose proof (eqv_contains 1 eq_refl _ _ e) as H. (* H: contains 1 (C n) = contains 1 (C 1) *)
simpl in H.
apply PeanoNat.Nat.eqb_eq in H.
symmetry; exact H.
Qed.


#### Notification Bot (Oct 28 2022 at 22:57):

yicx has marked this topic as resolved.

Last updated: Jun 18 2024 at 09:02 UTC