The Coq mailing list

[Matthieu Sozeau <mattam AT mattam.org>]

Hi Benedikt,

Le 3 mars 10 à 11:57, ben a écrit :

> Hello,
>
> I am working on a formalisation of the category Delta, i.e. sets of
> naturals smaller than a given natural, and weakly monotone functions
> between them.
>
> Given two monotone functions, I can place them side by side. This  
> should
> again give a monotone functions between the sums of sources and  
> targets,
> resp.
>
> The last definition of the theory on the bottom is my attempt to  
> define
> this "sum" of functions. It is done using Program, since there are a  
> lot
> of proof obligations involved.
> Unfortunately I don't succeed in solving the last obligation
> (monotonicity of the sum of functions), where I would like to distinct
> two cases (c.f. the code).
>
> How could I solve this last obligation ?

<snip/>

> Variables m m' n n': nat.
> Variable f: HomDelta n n'.
> Variable g: HomDelta m m'.
>
>
> Program Definition plus_morphism : HomDelta (n + m) (n' + m') :=
>         fun i => match le_lt_dec n i with
>                  | right _ => f i
>                  | left _ => n' + g (i - n)
>                  end.
>
>  Next Obligation.
>    Proof. apply cod_wd2. Defined.
>
>  Next Obligation.
>    Proof. apply lt_minus.
>           rewrite plus_comm.
>           apply (proj2_sig i).
>           auto.
>   Defined.
>
>  Next Obligation.
>    Proof. apply lt_plus_left.
>           apply cod_wd.
>    Defined.
>
>  Next Obligation.
>    Proof. unfold monotone. intros x y H.
>           (* case (le_lt_dec n x). *)
>           (* would be what i'd like to have *)

You have a problem of dependency here. As the obligations have types
mentionning proofs of [x = le_lt_dec .. ..], you cannot generalize  
le_lt_dec
here. One way to eliminate this dependency is to unfold the obligations,
(using [autounfold with plus_morphism in *] in 8.3) or to avoid this
unnecessary dependency using an [if then else] instead of a [match] in
the definition. When matching [le_lt_dec n i], you don't actually need  
to
keep an equality between the call and the branches patterns as all the
important logical information is kept in the result of [le_lt_dec n i].
Another way to deactivate the generation of this equality is to write
[match le_lt_dec n i return _] which forces the inference of the  
predicate
in the usual way.

Hope this helps,
-- Matthieu