How can I correspond a hypothesis to a decidable axiom in match (in Coq)?

Question

I made some record structure $I$ with addition and equality. And I made an axiom.

Axiom I_dec : 
forall a : I, ({0 < a} + {a < 0}) + {a == 0}.

With this axiom, I define a multiplication of $I$.

Definition I_seq_mult_l (a b : I) := 
match (I_dec a) with 
 | inleft (left H) => 
   match (I_dec b) with 
    | inleft (left H) => ...
    | inleft (right H) => ...
    | inright H => ...
   end
 | inleft (right H) => 
   match (I_dec b) with 
    | inleft (left H) => ...
    | inleft (right H) => ...
    | inright H => ...
   end 
 | inright H => ...
end.

When I prove some lemma, I meet an unsolved situation.

1 goal
a, b : I
Ha : const_I 0 < a
Hb : const_I 0 < b
Hb' : - b < const_I 0
______________________________________(1/1)
(exists m : positive,
   forall n : positive,
   (m <= n)%positive ->
   -
   match I_dec (- b) with
   | inleft (left _) => ...
   | inleft (right _) =>
       fun n0 : positive => ...
   | inright _ => ...
   end n <= r a n * r b n)

Previously, I destruct (I_dec a) and (I_dec b).

destruct (I_dec a) as [[Ha|Ha]|Ha], (I_dec b) as [[Hb|Hb]|Hb].

I made a hypothesis Hb' from Hb. And I think Hb' implies that I_dec (- b) match with inleft (right _).

So I want to write 'simpl' and make this goal simple.

However, I can't do this. So, I destruct (I_dec (- b)) also. It multiplies steps three times.

Can I match a processed hypothesis with a part of a decidable axiom?

Answer 1

If you think that Hb' implies that I_dec (-b) matches with inleft (right _)… then you should just prove that. Something like

Lemma lt0 {a : I} : a < 0 -> exists p, I_dec a = inleft (right p)

Even better, if you happen to have some uniqueness of proofs, you might prove

Lemma lt0 {a : I} (H : a < 0), I_dec a = inleft (right H)

To prove this, you will probably need extra axioms on <, stating that it is irreflexive and transitive.

In your setting you could then use the lemma, with something like

destruct (lt0 Hb') as [? ->].

This uses the lemma to replace the I_dec (-b) in your goal by inleft (right p) for some variable p you just introduced. Then you can use simpl and have the goal simplified as you hope.

If this situation turns up often (and I guess it will if you have a lot of these definitions around), you might want some automated tactic to do this for you. You could try something like

Lemma lt0 {a : I} : a < 0 -> exists p, I_dec a = inleft (right p).
…

Lemma gt0 {a : I} : 0 < a -> exists p, I_dec a = inleft (left p).
…

Lemma eq0 : exists p, I_dec z = inright p.
…

Ltac simp_dec :=
  repeat (match goal with
    | H : lt ?a z |- context [I_dec ?a] => destruct (lt0 H) as [p ->] ; clear p
    | H : lt z ?a |- context [I_dec ?a] => destruct (gt0 H) as [p ->] ; clear p
    | H : 
    | |- context [I_dec z] => destruct eq0 as [p ->] ; clear p
  end) ; simpl.

This tactic repeatedly replaces the I_dec _ appearing in your terms until there are none left, and simplifies the whole term at the end.