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

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?

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.