The Coq mailing list

[brandon_m_moore AT yahoo.com]

I've found ring helpful for solving equations between boolean conjunctions.
It would be nice if it would simplify repeated terms.
I was thinking I could do this be registering the trivial "power" function b ^
n = b || (n > 0).

In preparation for messing with power_tac, I tried to make my own boolean type
and declare a ring over it. All the proofs and the Add Ring declaration go
through
without trouble, but attempting to use ring afterwards produces a large error
message.

Require Import Ring.

Inductive bool2 : Set := t | f.
Definition xor2 a b :=
  match a, b with
  | t, t => f
  | t, f => t
  | f, t => t
  | f, f => f
  end.
Definition and2 a b :=
  match a with
  | t => b
  | f => f
  end.
Definition eq2 a b :=
  match a, b with
  | t, t => true
  | t, f => false
  | f, t => false
  | f, f => true
  end.
Lemma eq2_prop a b : eq2 a b = true -> a = b.
Proof. destruct a; destruct b; simpl; congruence. Qed.

Definition bool2_pow (b : bool2) (pow : BinNat.N) : bool2 :=
  match pow with
  | BinNat.N0 => t
  | BinNat.Npos _ => b
  end.
Lemma and2_idem (b : bool2) : and2 b b = b.
destruct b; reflexivity. Qed.
Lemma bool_pow_pow : Ring_theory.power_theory t and2 (@eq _) (@id _) 
bool2_pow.
constructor. intros. destruct n; simpl. reflexivity.
pose proof (and2_idem r). induction p; simpl; congruence.
Qed.
Ltac ignore_bool2_powers e := InitialRing.NotConstant.

Lemma bool2_ring : ring_theory f t xor2 and2 xor2 (@id _) (@eq _).
Proof.
constructor; repeat (intros b; destruct b; try reflexivity).
Qed.

Add Ring bring : bool2_ring (decidable eq2_prop).
(*  power_tac bool_pow_pow [ignore_bool2_powers]). *)

Lemma test (b : bool2) : and2 b b = b.
ring.

This produces an error:

In nested Ltac calls to "F" (bound to PackRing ltac:Ring_gen), "PackRing",
"F" (bound to
fun RNG lH rl =>
  let lemma := get_NormLemma RNG in
  get_Pre RNG (); Ring RNG (lemma ring_subst_niter) lH), "Ring",
"OnEquation", "f" (bound to
fun lhs rhs =>
  let mkFV := get_RingFV RNG in
  let mkPol := get_RingMeta RNG in
  let mkHyp := get_RingHypTac RNG in
  let fv := FV_hypo_tac mkFV ltac:(get_Eq RNG) lH in
  let fv := mkFV lhs fv in
  let fv := mkFV rhs fv in
  ListTactics.check_fv fv;
   (let pe1 := mkPol lhs fv in
    let pe2 := mkPol rhs fv in
    let lpe := mkHyp fv lH in
    let vlpe := fresh "hyp_list" in
    let vfv := fresh "fv_list" in
    pose (vlpe := lpe); pose (vfv := fv);
     apply (lemma vfv vlpe pe1 pe2) || fail
      "typing error while applying ring";
     [ (let prh := proofHyp_tac lH in
        exact prh) || idtac "can not automatically proof hypothesis :"; idtac
        " maybe a left member of a hypothesis is not a monomial"
     | vm_compute; exact (eq_refl true) || fail "not a valid ring equation"
])),
"mkFV" (bound to
fun t fv =>
  let rec TFV t fv :=
   (let f :=
     (match Cst t with
      | NotConstant =>
          match t with
          | add ?t1 ?t2 => fun _ => TFV t2 ltac:(TFV t1 fv)
          | mul ?t1 ?t2 => fun _ => TFV t2 ltac:(TFV t1 fv)
          | sub ?t1 ?t2 => fun _ => TFV t2 ltac:(TFV t1 fv)
          | opp ?t1 => fun _ => TFV t1 fv
          | pow ?t1 ?n =>
              match CstPow n with
              | NotConstant => fun _ => ListTactics.AddFvTail t fv
              | _ => fun _ => TFV t1 fv
              end
          | _ => fun _ => ListTactics.AddFvTail t fv
          end
      | _ => fun _ => fv
      end) in
    f ()) in
  TFV t fv), "TFV" (bound to
fun t fv =>
  let f :=
   (match Cst t with
    | NotConstant =>
        match t with
        | add ?t1 ?t2 => fun _ => TFV t2 ltac:(TFV t1 fv)
        | mul ?t1 ?t2 => fun _ => TFV t2 ltac:(TFV t1 fv)
        | sub ?t1 ?t2 => fun _ => TFV t2 ltac:(TFV t1 fv)
        | opp ?t1 => fun _ => TFV t1 fv
        | pow ?t1 ?n =>
            match CstPow n with
            | NotConstant => fun _ => ListTactics.AddFvTail t fv
            | _ => fun _ => TFV t1 fv
            end
        | _ => fun _ => ListTactics.AddFvTail t fv
        end
    | _ => fun _ => fv
    end) in
  f ()) and "Cst" (bound to fun t => match t with
                                     | rO => cO
                                     | rI => cI
                                     end), last call failed.
Error: No matching clauses for match.