The Coq mailing list

[Pierre Casteran <pierre.casteran AT labri.fr>]

Selon Houda Anoun 
<anoun AT labri.fr>:


Hi Houda.

 May be that the problems comes from the use of two kinds of polymorphism
(one with dependent product (ML-like), and functor polymorphism).

I don't know if the following example will help you, but here is
a definition of a module type for Comparable sets, and a functor
which build (comparable) formulae.

It is highly incomplete wrt to your goals, but I hope it can help
a little.

Pierre


(* Totally ordered set *)

Module Type TOSET.
 Parameter t : Set.
 Parameter compare : t -> t -> comparison.
 Axiom compare_eq : forall a b, compare a b = Eq -> a = b.
 Axiom compare_eq2 : forall a, compare a a = Eq.
End TOSET.


(* Simple formulae *)

Module Form (T:TOSET) <: TOSET.

 Inductive form : Set :=
   atom : T.t -> form
 | impl : form -> form -> form.

 Definition t := form.


 Fixpoint compare (f1 f2:t){struct f1}: comparison :=
  match (f1,f2) with (atom a1, atom a2) => T.compare a1 a2
                   | (impl f1 f2, impl f3 f4) =>
                          (match compare f1 f3 with Lt => Lt
                                                    | Gt => Gt
                                                    | Eq =>
                                                      compare f2 f4
                           end)
                   | (atom a, impl f3 f4)=> Lt
                   | (_,_)               => Gt
  end.

 Theorem  compare_eq : forall a b, compare a b = Eq -> a = b.
 Proof.
  induction a; destruct b.
  unfold compare.
 intro;  rewrite  (T.compare_eq t0 t1); auto.
 simpl.
 discriminate 1.
 simpl;discriminate 1.
 simpl.
 (* thank you Yves *)
 Ltac caseEq f := generalize (refl_equal f); pattern f at -1; case f.
 caseEq (compare a1 b1); caseEq (compare a2 b2); try discriminate 3.
 intros H0 H1;rewrite (IHa1 b1 H1);rewrite (IHa2 b2 H0); auto.
Qed.

Lemma compare_eq2 : forall a, compare a a  = Eq.
Proof.
 induction a.
 unfold compare;rewrite (T.compare_eq2 t0);auto.
 simpl;rewrite IHa1.
 rewrite IHa2.
 auto.
Qed.


End Form.




-- 
Pierre Casteran
(+33) 540006931

----------------------------------------------------------------
This message was sent using IMP, the Internet Messaging Program.