The Coq mailing list

[Jean Goubault-Larrecq <Jean.Goubault AT dyade.fr>]

Simao Desousa wrote:
> Let me explain my problem with a dummy example:
> Given two sets A and B, I state, by an hypothesis,
> that I have a function f from A to (Exc B).
> I define a function g by case analysis upon the result of f.
> 
> Definition g:=[x:A] Cases (f x) of
>                      (value  u) => ....
>                    |  _ => ....
>                   end.
> 
> For proving properties of g by case analysis,
> [...]

        The standard solution (to me at least) is
to prove an auxiliary lemma:


Lemma sumbool_of_exc : (A:Set) (x : (Exc A)) {a:A | x=(value A
a)}+{x=(error A)}.
Proof.
  Induction x. Intro. Left. Exists y. Reflexivity.
  Right. Reflexivity.
Qed.

Then to prove properties of g, assuming (f x) is of type (Exc B), do:
Elim (sumbool_of_exc B (f x)); Intros.

In the first branch, you'll get an assumption H23 (or whatever) of
type {a:B | (f x)=(value B a)}.  Do Elim H23; Intros.  This will
produce an assumption H25 : (f x)=(value B a).  Then do Rewrite H25.
This simplifies your goal and you can continue your proof on this
branch.

In the second branch, you'll get an assumption H23 : (f x)=(error B).
Then Rewrite H23.

(I do this usually on booleans, using sumbool_of_bool as provided in
BOOL/Sumbool.  The above is just imitation of that case.)

By the way, if you do this often, you can automate it:

Tactic Definition DecExc [$B $expr $H1 $u $H2] :=
   [<:tactic:<Elim (sumbool_of_exc $B $expr);
                   [(Intro $H1; Elim $H1; Intros $u $H2; Rewrite $H2) |
                    (Intro $H2; Rewrite $H2)]>>].

(Usage: DecExc B (f x) H1 u H2
 Caution: will only work provided you have no variable H1, u or H2
 in your current context.)


Example:
Lemma gag : (A:Set) (x:(Exc A))
  (Cases x of (value u) => (value A u) | error => (error A) end)=x.
Proof.
  Intros A x.
  DecExc ? x H1 u H2. (* Note that wildcards like ? still work. *)
  Reflexivity.
  Reflexivity.
Qed.

        All the best,

        -- Jean.