✔ question about eqv to eq · Coq users

================================================
From Coq Require Import 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?

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):

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):

Thanks everyone for your idea,
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):

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.

Stream: Coq users

Topic: ✔ question about eqv to eq

yicx (Oct 26 2022 at 00:29):