Require Import ADPUnif. Require Import ADecomp. Require Import ADuplicateSymb. Require Import AGraph. Require Import APolyInt_MA. Require Import ATrs. Require Import List. Require Import LogicUtil. Require Import MonotonePolynom. Require Import Polynom. Require Import SN. Require Import VecUtil. Open Scope nat_scope. (* termination problem *) Module M. Inductive symb : Type := | _0_1 : symb | f : symb | g : symb | minus : symb | s : symb. End M. Lemma eq_symb_dec : forall f g : M.symb, {f=g}+{~f=g}. Proof. decide equality. Defined. Open Scope nat_scope. Definition ar (s : M.symb) : nat := match s with | M._0_1 => 0 | M.f => 1 | M.g => 1 | M.minus => 2 | M.s => 1 end. Definition s0 := ASignature.mkSignature ar eq_symb_dec. Definition s0_p := s0. Definition V0 := @ATerm.Var s0. Definition F0 := @ATerm.Fun s0. Definition R0 := @ATrs.mkRule s0. Module S0. Definition _0_1 := F0 M._0_1 Vnil. Definition f x1 := F0 M.f (Vcons x1 Vnil). Definition g x1 := F0 M.g (Vcons x1 Vnil). Definition minus x2 x1 := F0 M.minus (Vcons x2 (Vcons x1 Vnil)). Definition s x1 := F0 M.s (Vcons x1 Vnil). End S0. Definition E := @nil (@ATrs.rule s0). Definition R := R0 (S0.minus (V0 0) S0._0_1) (V0 0) :: R0 (S0.minus (S0.s (V0 0)) (S0.s (V0 1))) (S0.minus (V0 0) (V0 1)) :: R0 (S0.f S0._0_1) (S0.s S0._0_1) :: R0 (S0.f (S0.s (V0 0))) (S0.minus (S0.s (V0 0)) (S0.g (S0.f (V0 0)))) :: R0 (S0.g S0._0_1) S0._0_1 :: R0 (S0.g (S0.s (V0 0))) (S0.minus (S0.s (V0 0)) (S0.f (S0.g (V0 0)))) :: @nil (@ATrs.rule s0). Definition rel := ATrs.red_mod E R. (* symbol marking *) Definition s1 := dup_sig s0. Definition s1_p := s0. Definition V1 := @ATerm.Var s1. Definition F1 := @ATerm.Fun s1. Definition R1 := @ATrs.mkRule s1. Module S1. Definition h_0_1 := F1 (hd_symb s1_p M._0_1) Vnil. Definition _0_1 := F1 (int_symb s1_p M._0_1) Vnil. Definition hf x1 := F1 (hd_symb s1_p M.f) (Vcons x1 Vnil). Definition f x1 := F1 (int_symb s1_p M.f) (Vcons x1 Vnil). Definition hg x1 := F1 (hd_symb s1_p M.g) (Vcons x1 Vnil). Definition g x1 := F1 (int_symb s1_p M.g) (Vcons x1 Vnil). Definition hminus x2 x1 := F1 (hd_symb s1_p M.minus) (Vcons x2 (Vcons x1 Vnil)). Definition minus x2 x1 := F1 (int_symb s1_p M.minus) (Vcons x2 (Vcons x1 Vnil)). Definition hs x1 := F1 (hd_symb s1_p M.s) (Vcons x1 Vnil). Definition s x1 := F1 (int_symb s1_p M.s) (Vcons x1 Vnil). End S1. (* graph decomposition 1 *) Definition cs1 : list (list (@ATrs.rule s1)) := ( R1 (S1.hminus (S1.s (V1 0)) (S1.s (V1 1))) (S1.hminus (V1 0) (V1 1)) :: nil) :: ( R1 (S1.hg (S1.s (V1 0))) (S1.hminus (S1.s (V1 0)) (S1.f (S1.g (V1 0)))) :: nil) :: ( R1 (S1.hf (S1.s (V1 0))) (S1.hminus (S1.s (V1 0)) (S1.g (S1.f (V1 0)))) :: nil) :: ( R1 (S1.hf (S1.s (V1 0))) (S1.hg (S1.f (V1 0))) :: R1 (S1.hg (S1.s (V1 0))) (S1.hf (S1.g (V1 0))) :: R1 (S1.hf (S1.s (V1 0))) (S1.hf (V1 0)) :: R1 (S1.hg (S1.s (V1 0))) (S1.hg (V1 0)) :: nil) :: nil. (* polynomial interpretation 1 *) Module PIS1 (*<: TPolyInt*). Definition sig := s1. Definition trsInt f := match f as f return poly (@ASignature.arity s1 f) with | (hd_symb M.minus) => (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (int_symb M.minus) => (2%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M._0_1) => nil | (int_symb M._0_1) => (3%Z, Vnil) :: nil | (hd_symb M.s) => nil | (int_symb M.s) => (2%Z, (Vcons 0 Vnil)) :: (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.f) => nil | (int_symb M.f) => (1%Z, (Vcons 0 Vnil)) :: (3%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.g) => nil | (int_symb M.g) => (3%Z, (Vcons 0 Vnil)) :: (3%Z, (Vcons 1 Vnil)) :: nil end. Lemma trsInt_wm : forall f, pweak_monotone (trsInt f). Proof. pmonotone. Qed. End PIS1. Module PI1 := PolyInt PIS1. (* polynomial interpretation 2 *) Module PIS2 (*<: TPolyInt*). Definition sig := s1. Definition trsInt f := match f as f return poly (@ASignature.arity s1 f) with | (hd_symb M.minus) => nil | (int_symb M.minus) => (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M._0_1) => nil | (int_symb M._0_1) => nil | (hd_symb M.s) => nil | (int_symb M.s) => (1%Z, (Vcons 0 Vnil)) :: (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.f) => (1%Z, (Vcons 1 Vnil)) :: nil | (int_symb M.f) => (1%Z, (Vcons 0 Vnil)) :: (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.g) => (1%Z, (Vcons 1 Vnil)) :: nil | (int_symb M.g) => (1%Z, (Vcons 1 Vnil)) :: nil end. Lemma trsInt_wm : forall f, pweak_monotone (trsInt f). Proof. pmonotone. Qed. End PIS2. Module PI2 := PolyInt PIS2. (* graph decomposition 2 *) Definition cs2 : list (list (@ATrs.rule s1)) := ( R1 (S1.hf (S1.s (V1 0))) (S1.hg (S1.f (V1 0))) :: nil) :: nil. (* termination proof *) Lemma termination : WF rel. Proof. unfold rel. dp_trans. mark. let D := fresh "D" in let R := fresh "R" in set_rules_to D; set_mod_rules_to R; graph_decomp (dpg_unif_N 100 R D) cs1; subst D; subst R. dpg_unif_N_correct. right. PI1.prove_termination. termination_trivial. left. co_scc. left. co_scc. right. PI2.prove_termination. let D := fresh "D" in let R := fresh "R" in set_rules_to D; set_mod_rules_to R; graph_decomp (dpg_unif_N 100 R D) cs2; subst D; subst R. dpg_unif_N_correct. left. co_scc. Qed.