The Coq mailing list

[Ian Lynagh <igloo AT earth.li>]

On Wed, Mar 04, 2009 at 04:01:01PM -0800, Taral wrote:
> 
> Exactly. In Ltac, this is the difference between "case" and "case_eq".
> I think it's a serious shortcoming of C-zar that it doesn't generate
> the equality.

I've had some success by making (X \/ Y) lemmas, and using "per cases
of" ("of" rather than "on") with them. It's a bit more verbose, but it
seems to work.

However, there are still a couple of hurdles I haven't managed to
overcome, marked with
    (* THIS IS NOT ACCEPTED *)
in the script below.


Variable U : Set.

Variable f : U -> option U.

Axiom finv : forall (u : U) (u' : U),
             (f u = Some u') -> (f u' = Some u).

Theorem NoneOrSome : forall (T : Set) (o : option T),
    (o = None) \/ (exists t : T, o = Some t).
proof.
let T : Set, o : (option T).
per cases on o.
suppose it is None.
    hence thesis.
suppose it is (Some t').
    focus on (exists t : T, Some t' = Some t).
        take t'.
        hence thesis.
    end focus.
end cases.
end proof.
Qed.

Inductive N : Set := MkN : U -> N.

Definition g (n : N) : option N
 := match n with
    MkN u =>
        match f u with
        | Some u' => Some (MkN u')
        | None => None
        end
    end.

Lemma MyLemma :
      forall (n : N)
             (n' : N),
      (g n  = Some n'
    -> g n' = Some n).
proof.
let n : N,
    n' : N.
assume H1 : (g n = Some n').
consider u:U from n.
then H2 : (n = MkN u). (* THIS IS NOT ACCEPTED *)
consider u':U from n'.

per cases of
    ((f u = None) \/ (exists u'' : U, f u = Some u''))
by NoneOrSome.
suppose H3 : (f u = None).
    then (f u = None).
    then (g (MkN u) = g (MkN u)).
      =~ match (MkN u) with
         (MkN u) =>
             match f u with
             | Some u' => Some (MkN u')
             | None => None
             end
         end.
      =~ match f u with
         | Some u' => Some (MkN u')
         | None => None
         end.
      =~ match None with
         | Some u' => Some (MkN u')
         | None => None
         end by H3. (* THIS IS NOT ACCEPTED *)
      =~ None.
    then (g (MkN u) = None).
    then H4 : (g n = None) by H2.
    thus thesis by H1, H4.
suppose H5 : (exists u'' : U, f u = Some u'').
(* Haven't done this case yet *)
thus thesis.
end cases.
Admitted.



Thanks
Ian