Library CoLoR.HORPO.HorpoExNonTrans

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 := a | b | c.

  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
    | a => #Star
    | b => #Star
    | c => #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
        | a, b => 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 HorpoNotTrans.

  Definition t1p := (\#Star => (^c [ %0 ])) @@ ^a.
  Definition t2p := (\#Star => (^c [ %0 ])) @@ ^b.
  Definition t3p := ^c [ ^b ].

  Definition t1 : nil |- t1p := #Star.


  Definition t2 : nil |- t2p := #Star.


  Definition t3 : nil |- t3p := #Star.


  Lemma horpo_not_trans : ~transitive horpo.

End HorpoNotTrans.