Library CoLoR.HORPO.HorpoExMap

CoLoR, a Coq library on rewriting and termination. See the COPYRIGHTS and LICENSE files.
  • Adam Koprowski, 2009-01-22


Module BT <: BaseTypes.

  Inductive BaseType_aux := Star.

  Definition BaseType := BaseType_aux.

  Lemma eq_BaseType_dec : forall A B : BaseType, {A = B} + {A <> B}.

  Lemma baseTypesNotEmpty : BaseType.

End BT.

Module Sig <: Signature.

  Module BT := BT.

  Module Export ST := SimpleTypes BT.

  Inductive FunctionSymbol_aux := nil | cons | map.

  Definition FunctionSymbol := FunctionSymbol_aux.

  Lemma eq_FunctionSymbol_dec :
    forall f g : FunctionSymbol, {f = g} + {f <> g}.

  Lemma functionSymbolsNotEmpty : FunctionSymbol.

  Definition f_type (f : FunctionSymbol) :=
    match f with
    | nil => #Star
    | cons => #Star --> #Star --> #Star
    | map => #Star --> (#Star --> #Star) --> #Star
    end.

End Sig.

Module Terms := Terms Sig.

Module P <: Precedence.

  Module Import S := Sig.

  Module FS <: SetA.
    Definition A := Sig.FunctionSymbol.
  End FS.

  Module Import FS_eq := Eqset_def FS.

  Module Import P <: Poset.

    Definition A := A.

    Module Export O <: Ord.

      Module S := FS_eq.

      Definition A := A.

      Definition gtA f g :=
        match f, g with
        | map, cons => True
        | _, _ => False
        end.

      Definition gtA_eqA_compat := @Eqset_def_gtA_eqA_compat A gtA.

    End O.

    Lemma gtA_so : strict_order gtA.

  End P.

  Lemma Ord_wf : well_founded (transp gtA).

  Lemma Ord_dec : forall a b, {gtA a b} + {~gtA a b}.

End P.

Module Horpo := HorpoWf Sig P.

Import Horpo.HC.


Section HorpoMap.

  Definition env_1 := (#Star --> #Star) [#] EmptyEnv.
  Definition rule_1_l := ^map [^nil, %0].
  Definition rule_1_r := ^nil.

  Definition env_2 := #Star [#] #Star [#] (#Star --> #Star) [#] EmptyEnv.
  Definition rule_2_l := ^map [^cons [%0, %1], %2].
  Definition rule_2_r := ^cons [%2 @@ %0, ^map [%1, %2]].

  Definition t_1_l : env_1 |- rule_1_l := #Star.


  Definition t_1_r : env_1 |- rule_1_r := #Star.


  Definition t_2_l : env_2 |- rule_2_l := #Star.


  Definition t_2_r : env_2 |- rule_2_r := #Star.


  Lemma rule_1 : buildT t_1_l >> buildT t_1_r.

  Lemma rule_2 : buildT t_2_l >> buildT t_2_r.

End HorpoMap.