Library Gamma


Require Export Pow.

Require Export LatticeAtom.




Set Implicit Arguments.




Record Gamma (A:Type) (B:Set) (PA:Poset A) (PB:Lattice B) : Type := gamma_constr {

  gamma_func :> B -> A;

  gamma_monotone : forall b1 b2, order PB b1 b2 -> 

                                 order PA (gamma_func b1) (gamma_func b2)

}.




Record GammaTop (A:Type) (B:Set) (PA:Poset A) (PB:Lattice B) : Type := gammatop_constr {

  gammatop_gamma :> Gamma PA PB;

  gamma_top : forall A, order PA A (gammatop_gamma (top PB))

}.




Record GammaBestTop (A:Set) (B:Set) (PB:LatticeAtom B) : Type := gammabesttop_constr {

  gammabesttop_gamma :> GammaTop (PowPoset A) PB;

  gamma_best : forall p b a,

    gammabesttop_gamma (best PB p) a ->

    gammabesttop_gamma b a ->

    in_set p (to_set PB b) = true;

  gamma_best_exist : forall b a,

    gammabesttop_gamma b a ->

    ~ to_set PB b = None ->

    exists p, gammabesttop_gamma (best PB p) a

}.




Definition orderGamma (A:Type) (B:Set) (PA:Poset A) (PB:Lattice B) (g1 g2:Gamma PA PB) :=

 forall b, order PA (g1 b) (g2 b).




Lemma orderGamma_refl : forall  (A:Type) (B:Set) (PA:Poset A) (PB:Lattice B) (g:Gamma PA PB),

  orderGamma g g.

Proof.

  intros.

  intros b; auto.

Qed.




Definition GammaMonotone 

  (C:Type) (A:Type) (B:Set) (PA:Poset A) (PB:Lattice B) (g:C->(Gamma PA PB))

  (R:C->C->Prop) := forall tr1 tr2,

    R tr1 tr2 -> orderGamma (g tr1) (g tr2).




Lemma GammaMonotone_incl : forall (C:Type) (A:Type) (B:Set) (PA:Poset A) (PB:Lattice B) (g:C->(Gamma PA PB))

  (R1 R2:C->C->Prop), 

 (forall x y, R1 x y -> R2 x y) ->

 (GammaMonotone g R2) -> (GammaMonotone g R1).

intros.

intros tr1; intros; auto.

Qed.
Index
This page has been generated by coqdoc