The Coq mailing list

[ben <Benedikt.Ahrens AT unice.fr>]

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 ?

Remark: the section "some_lemmata" can be ignored for this question.

Greetings
ben


Require Import Arith Compare_dec Omega Program.

Set Implicit Arguments.
Unset Strict Implicit.

(** the set of naturals smaller than n *)

Section N_set.

Variable n:nat.

Definition N_set := {m | m < n}.

Definition projTT : N_set -> nat :=
     fun x => proj1_sig x.

Coercion projTT : N_set >-> nat.

End N_set.

Notation "[[ n ]]" := (N_set n).


(** weakly monotone functions [[m]] -> [[n]] *)

Section delta_maps.

Variables m n: nat.

Definition monotone (f: [[m]] -> [[n]]) :=
          forall x y: [[m]], x <= y -> f x <= f y.

Definition HomDelta := { f : [[m]] -> [[n]] | monotone f }.

Definition forget_mon (f: HomDelta) :=
                proj1_sig f.

Coercion forget_mon: HomDelta >-> Funclass.

End delta_maps.



Section some_lemmata.

Lemma cod_wd: forall m n (f: [[m]] -> [[n]]) (x:[[m]]),
                   f x < n.
Proof. intros m n f x. destruct (f x).
        simpl. auto. Qed.

Lemma cod_wd2: forall m n (f: [[m]] -> [[n]]) (x: [[m]]),
               forall k:nat,  f x < n + k.
Proof. intros m n f x k.
       assert (f x < n).
       apply cod_wd.
       apply le_trans with n; auto. auto with arith.
Qed.

Lemma lt_minus: forall i m n, i < m + n -> n <= i -> i - n < m.
Proof. induction n. intros H0 H1. omega.
       omega.
Qed.

Lemma lt_plus_right : forall m n, m < n -> forall i, m + i < n + i.
Proof. induction m. intros n H i. omega.
                    intros n H i. omega.
Qed.

Lemma lt_plus_left: forall m n, m < n -> forall i, i + m < i + n.
Proof. induction m. intros n H i. omega.
                    intros n H i. omega.
Qed.

End some_lemmata.

(** "placing two morphisms side by side" should give
      a morphism *)

Section plus_on_morphisms.

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 *)