Stream: Coq users

Topic: ✔ question about eqv to eq


view this post on Zulip 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.
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!

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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 Z/2Z\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.

view this post on Zulip 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!

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Notification Bot (Oct 28 2022 at 22:57):

yicx has marked this topic as resolved.


Last updated: Oct 03 2023 at 21:01 UTC