# Library CoLoR.Term.WithArity.MonAlgChecker

CoLoR, a Coq library on rewriting and termination. See the COPYRIGHTS and LICENSE files.
This file contains a proof checker for termination criteria based
on (extended) weakly monotone algebra.

Set Implicit Arguments.

Section MonAlgChecker.

Variable Sig : Signature.

Notation Problem := (Problem Sig).
Notation term := (term Sig).
Notation rule := (@rule Sig).
Notation rules := (@list rule).

Variable domain : Type.
Let D := domain.
Variable domain_elt : D.

Variable succ : relation D.
Variable succeq : relation D.
Variable succ_wf : WF succ.
Variable succ_succeq_compat : absorbs_left succ succeq.

Variable arSymInt : nat -> Set.
Notation symInt := (symInt Sig arSymInt).
Notation funInt := (funInt Sig arSymInt).

Variable defaultInt : forall n, arSymInt n.

Variable interpret : forall n, arSymInt n -> naryFunction1 domain n.

Program Definition makeI (int : forall f, funInt f) :=
mkInterpretation (Sig:=Sig) domain_elt (fun f => interpret (int f)).

Variable check_succ : forall i r, option (IR (makeI i) succ (lhs r) (rhs r)).
Variable check_succeq : forall i r, option (IR (makeI i) succeq (lhs r) (rhs r)).

Section given_int.

Variable i : forall f, funInt f.
Notation I := (makeI i).

Notation IR_succ := (IR I succ).
Notation IR_succeq := (IR I succeq).

Section reduction_pairs.

Variable wm : monotone I succeq.

Lemma wf_IR_succ : WF IR_succ.

Lemma absorb_succ_succeq : absorbs_left IR_succ IR_succeq.

Definition wrp := mkWeak_reduction_pair
(IR_substitution_closed (I:=I) (R:=succ))
(IR_substitution_closed (I:=I) (R:=succeq))
(IR_context_closed wm) absorb_succ_succeq wf_IR_succ.

Section sm.

Variable sm : monotone I succ.

Definition rp := mkReduction_pair
(IR_substitution_closed (I:=I) (R:=succ))
(IR_substitution_closed (I:=I) (R:=succeq))
(IR_context_closed sm) (IR_context_closed wm)
absorb_succ_succeq wf_IR_succ.

End sm.

End reduction_pairs.

Section prover.

Variable check_int_wm : option (monotone I succeq).
Variable check_int_sm : option (monotone I succeq /\ monotone I succ).

Program Definition check_compat (R : rules) (F : relation D)
(check_compat : forall i r, option (IR (makeI i) F (lhs r) (rhs r))) :
option (compat (IR (makeI i) F) R) :=
match lforall_opt _ (check_compat i) R with
| Some _ => Some _
| None => None
end.

Program Definition simplify (R : rules) :
option { Rge : rules |
exists Rgt : rules,
compat IR_succ Rgt /\
compat IR_succeq Rge /\
incl R (Rgt ++ Rge)
} :=
let (Rp, obl) := partition_opt _ (check_succ i) R in
match check_compat (snd Rp) check_succeq with
| None => None
| Some _ => Some (snd Rp)
end.

Program Definition applyMonotoneAlgebra (P : Problem) :
option { P' : Problem | Prob_WF P' -> Prob_WF P } :=

match P with
| FullTerm R =>
match check_int_sm with
| None => None
| Some sm =>
match simplify R with
| None => None
| Some R' => Some (FullTerm R')
end
end
| RelTopTerm T R =>
match check_int_wm with
| None => None
| Some wm =>
match check_compat T check_succeq with
| None => None
| Some _ =>
match simplify R with
| None => None
| Some R' => Some (RelTopTerm T R')
end
end
end
| RelTerm T R =>
match check_int_sm with
| None => None
| Some sm =>
match simplify T with
| None => None
| Some T' =>
match simplify R with
| None => None
| Some R' => Some (RelTerm T' R')
end
end
end
end.

End prover.

End given_int.

Record monSpec monR :=
{ monP : symInt -> Prop
; mon_check : forall (i : symInt), option (monP i)
; mon_ok : forall (i : symInt),
monP i -> Vmonotone1 (interpret (projT2 i)) monR
}.

Let buildSymInt := buildSymInt Sig arSymInt.
Let defaultIntForSymbol := defaultIntForSymbol Sig arSymInt defaultInt.

Variable wm : monSpec succeq.
Variable sm : monSpec succ.
Variable sm_imp_wm : forall s, monP sm s -> monP wm s.
Variable sm_default : forall f, (monP sm)
(buildSymInt (defaultIntForSymbol f)).

Lemma wm_default : forall f,
(monP wm) (buildSymInt (defaultIntForSymbol f)).

Section monotonicityChecker.

Variable i : list symInt.
Let I := (makeI (buildInt defaultInt i)).

Let buildInt := (buildInt defaultInt i).

Program Definition check_wm : option (monotone I succeq) :=
match @checkProp Sig arSymInt defaultInt
(monP wm) (mon_check wm) wm_default i with
| None => None
| Some _ => Some _
end.

Program Definition check_sm :
option (monotone I succeq /\ monotone I succ) :=
match @checkProp Sig arSymInt defaultInt
(monP sm) (mon_check sm) sm_default i with
| None => None
| Some _ => Some _
end.

End monotonicityChecker.

Section solver.

Variable rawSymInt : Type.
Variable rti : rawTrsInt Sig rawSymInt.
Variable check_ri : Sig -> rawSymInt -> option symInt.

Program Definition monotoneAlgebraSolver (P : Problem) :
option { P' : Problem | Prob_WF P' -> Prob_WF P } :=

match processInt check_ri rti with
| None => None
| Some fis =>
applyMonotoneAlgebra (check_wm fis) (check_sm fis) P
end.

End solver.

End MonAlgChecker.