The Coq mailing list

[Pierre Corbineau <pierre.corbineau AT laposte.net>]

in the second case :

The problem has to do with the automation used (the congruence tactic 
doesn't rewrite in match...with).

a workaround :
define C x as (match x with
        | Some u' => Some (MkN u')
           | None => None
        end.

        =~ (C (f u)).
        =~ (C None) by H3.
        =~ None.





Ian Lynagh a écrit :
> 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
>
> --------------------------------------------------------
> Bug reports: http://logical.saclay.inria.fr/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>           http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club