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.

Admitted.

================================================

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!

This needs some ingenuity. My intuition would be to give a somewhat normal form to `term`

s 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.

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`

.

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.

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!

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.
```

Thanks everyone for your idea,

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

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.
```

yicx has marked this topic as resolved.

Last updated: Jun 18 2024 at 09:02 UTC