The Coq mailing list

[Abhishek Anand <abhishek.anand.iitg AT gmail.com>]

Thanks for your perfect solutions to both the problems.

I was initially surprised by your solution to the second problem, which was about boolean rings.

I was expecting that I would have to instantiate forall x, x*x=x and  forall x, x+x =0 even for composite expressions and not just for variables.

However, it was easy to prove in Coq that the instances for composite expressions can be derived just from ring laws and the instances for atomic variables.

I have included the proof below.

It seems that I now have the complete decision procedure (for boolean rings) that I was looking for, except that I may have run into a bug in nsatz.

I have illustrated it in the lemma nsatzNotComplete below, where nsatz fails unexpectedly and succeeds if I reorder a hypothesis.

Is this a known limitation of nsatz, or just a bug?

Require Import Nsatz.

Require Import Omega.

Section test.

Context {R:Type}`{Rid:Integral_domain R}.

Lemma nsatzNotComplete : forall (a b :R),

a*a==a -> a+a==0 -> b*b==b ->  b+b==0 -> a*a*(b*b)==a*b.

Proof.

  intros. 

  try (nsatz; fail).

  move H0 after H1. (* why is this needed *)

  nsatz.

Qed.

Variable atomics: list R.

Definition interpretAtomic (n:nat) : R :=

  List.nth n (1::atomics) 0.

Inductive compositeRingExpr : Type :=

| injectAtomic (i : nat)

| cadd (cl cr : compositeRingExpr)

| cmult (cl cr : compositeRingExpr)

| cnegate (c: compositeRingExpr).

Fixpoint interpretComposite (c : compositeRingExpr) : R :=

match c with

| injectAtomic i => interpretAtomic i

| cmult cl cr => interpretComposite cl * interpretComposite cr

| cadd cl cr => interpretComposite cl + interpretComposite cr

| cnegate c => - (interpretComposite c)

end.

(** the proof would be by induction on a carefully designed size function.

structural induction doesn't work *)

Fixpoint size (c : compositeRingExpr) : nat :=

match c with

| injectAtomic i => 1

| cmult cl cr => 1 + size cl + size cr

(* it is critical to have the size of addition be larger than multiplication *)

| cadd cl cr => 2 + size cl + size cr

| cnegate c =>  1 + size c

end.

Definition booleanProps (c: R) : Prop := c*c==c /\ c+c==0.

Lemma booleanPropsComposites : 

(forall a:R, In a (0::1::atomics) -> booleanProps a)

->

(forall c:compositeRingExpr, booleanProps (interpretComposite c)).

Proof.

  intros Ha ?. remember (size c) as n. revert dependent c.

  induction n  as [n Hind] using lt_wf_ind.

  intros ? Heq.

  destruct c; auto; simpl;[clear Hind | clear Ha | clear Ha | clear Ha].

(* injectAtomic *)

- unfold interpretAtomic. apply Ha.

  destruct (nth_in_or_default i (1::atomics) 0) as [Hin | Hin]; simpl in *; auto.

(* cadd *)

- simpl in *. 

  pose proof (fun p => Hind (size c1) p c1) as H1.

  pose proof (fun p => Hind (size c2) p c2) as H2. clear Hind.

  destruct H1;  try omega.

  destruct H2;  try omega.

  split; nsatz.

(* cmult *)

- simpl in *. 

  pose proof (fun p => Hind (size c1) p c1) as H1.

  pose proof (fun p => Hind (size c2) p c2) as H2. clear Hind.

  destruct H1;  try omega.

  destruct H2;  try omega.

  split; try (nsatz ;fail).

  clear H0 H2. 

  (* nsatz is not monotonic? at least it spits a different error (could not prove discrimination result)

  instead of saying that the polynomial is not in the ideal *)

  nsatz.

- simpl in *. destruct (fun p => Hind (size c) p c); try omega.

  split; try nsatz. 

Qed.

Thanks,

-- Abhishek

http://www.cs.cornell.edu/~aa755/

On Wed, Apr 13, 2016 at 5:59 PM, Laurent Thery <Laurent.Thery AT inria.fr> wrote:

Not that I remember of, but calling ring with the equations x * x = x
for all the boolean variables of your _expression_ should do the trick.

Oops you should also add 2*x = 0.

- Laurent