Library CoLoR.Term.Lambda.LSystemT

CoLoR, a Coq library on rewriting and termination.
• Frederic Blanqui, 2013-09-17

Termination proof of Goedel System T

Set Implicit Arguments.

Type constants of System T.

Inductive B : Type := Nat : B.

Lemma eq_B_dec : forall a b : B, {a=b}+{~a=b}.

Typ structure for type constants.

Module BTyp <: Typ.

Definition t := B.

End BTyp.

Cmp structure for type constants.

Module BCmp <: Cmp.

Include BTyp.

Definition cmp (_ _ : B) := Eq.

Lemma cmp_opp x y : cmp x y = CompOpp (cmp y x).

End BCmp.

CmpTransLeibniz structure for type constants.

Module BCmpTransLeibniz <: CmpTransLeibniz.

Include BCmp.

Lemma cmp_eq x y : cmp x y = Eq -> x = y.

Lemma cmp_lt_trans x y z : cmp x y = Lt -> cmp y z = Lt -> cmp x z = Lt.

End BCmpTransLeibniz.

Types of System T.

Notation TNat := (Base Nat).

Cmp structure for System T types.

Module Ty_Cmp := ST_Cmp BCmp.

CmpTransLeibniz structure for System T types.

Function symbols of System T.

Inductive F : Type :=
| Zero : F
| Succ : F
| Rec : Ty B -> F.

Well-founded precedence on function symbols.

Definition prec f :=
match f with
| Zero => 0
| Succ => 1
| Rec _ => 2
end.

Cmp structure for function symbols.
We use the lexicographic path ordering with Zero < Succ < Rec A and Rec A < Rec B if A < B.

Module FCmp <: Cmp.

Definition t := F.

Fixpoint cmp f g :=
match f, g with
| Rec u, Rec v => Ty_Cmp.cmp u v
| _, _ => nat_compare (prec f) (prec g)
end.

Lemma cmp_opp f g : cmp f g = CompOpp (cmp g f).

End FCmp.

CmpTransLeibniz structure for function symbols.

Module FCmpTransLeibniz <: CmpTransLeibniz.

Include FCmp.

Lemma cmp_eq x y : cmp x y = Eq -> x = y.

Lemma cmp_lt_trans x y z : cmp x y = Lt -> cmp y z = Lt -> cmp x z = Lt.

End FCmpTransLeibniz.

OrderedType structure for function symbols.

L structure (term algebra) of System T.

Module L_SystemT <: L_Struct.

Definition F := F.

Module FOrd := FOrd.

Module Export V := NatVar.

Notation Te := (Te F X).
Notation Tes := (vector Te).

Notation Var := (@Var F X).
Notation Fun := (@Fun F X).
Notation App := (@App F X).
Notation Lam := (@Lam F X).

Notation apps := (@apps F X).
Notation fv := (@fv F X ens_X).
Notation eq_term_dec := (@eq_term_dec F X FOrd.eq_dec XOrd.eq_dec).

Notation FZero := (Fun Zero).
Notation FSucc := (Fun Succ).
Definition FRec A := Fun (Rec A).

End L_SystemT.

RS structure (rewrite rules) of System T.

Import VectorNotations.
Local Open Scope vector_scope.

Module RS_SystemT <: RS_Struct.

Module Export L := L_SystemT.

Definition u := Var 0.
Definition v := Var 1.
Definition n := Var 2.

Inductive R : relation Te :=
| rule_Rec_Zero : forall A, R (apps (Fun (Rec A)) [FZero; u; v]) u
| rule_Rec_Succ : forall A, R (apps (Fun (Rec A)) [apps FSucc [n]; u; v])
(apps v [n; apps (FRec A) [n; u; v]]).

Definition rule := R.

Instance fv_rule : Proper (rule --> Subset) fv.

Definition lhs_fun l r (_ : rule l r) :=
| Def.Fun f => f
| _ => Zero
end.

Definition lhs_nb_args l r (_ : rule l r) := 3.

Definition lhs_args l r :=
match l as l return forall h : rule l r, Tes (lhs_nb_args h) with
| Def.App (Def.App (Def.App (Def.Fun _) l1) l2) l3 =>
fun _ => [l1; l2; l3]
| _ => fun _ => [FZero; FZero; FZero]
end.

Lemma lhs_ok l r ( h : rule l r) : l = apps (Fun (lhs_fun h)) (lhs_args h).

End RS_SystemT.

ST structure (types of function symbols) of System T.

Module ST_SystemT <: ST_Struct.

Module Export L := L_SystemT.

Definition So := B.

Notation Ty := (Ty So).

Notation TNat := (Base Nat).

Fixpoint typ f :=
match f with
| Zero => TNat
| Succ => TNat ~~> TNat
| Rec A => TNat ~~> A ~~> (TNat ~~> A ~~> A) ~~> A
end.

Module Export XMap := FMapAVL.Make XOrd.

Notation En := (@XMap.t Ty).
Notation empty := (@XMap.empty Ty).
Notation In := (@XMap.In Ty).
Notation MapsTo := (@XMap.MapsTo Ty).
Notation Equal := (@XMap.Equal Ty).
Notation env := (mk_Env empty add In MapsTo Equal).

End ST_SystemT.

DLQO structure for the termination proof of System T.

We use prec to quasi-order function symbols in a wellfounded way.

Module DLQO_SystemT <: DLQO_Struct.

Module Export ST := ST_SystemT.

Definition C := F.

Definition code (f : F) := f.

Import FCmp.

Definition gtC := Rof gt prec.

Lemma gtC_wf : WF gtC.

Definition filter_arity (_ : F) := 1.

Definition filter (_ : F) := [0].

Notation gt_call := (@gt_call F X C code gtC).
Notation gt_args_lex := (@gt_args_lex F X FOrd.eq_dec XOrd.eq_dec ens_X
var_notin C filter_arity filter).

End DLQO_SystemT.

Wellfounded OrderedType structure on type constants.

We use the empty relation to quasi-order type constants in a wellfounded way.

Module BOrdWF_MOT <: MiniOrderedType.

Include BTyp.

Include LeibnizFacts BTyp.

Definition lt : relation t := empty_rel.

Instance lt_trans : Transitive lt.

Lemma lt_not_eq x y : lt x y -> x <> y.

Lemma compare x y : Compare lt eq x y.

End BOrdWF_MOT.

Module BOrdWF := MOT_to_OT BOrdWF_MOT.

BI structure (accessible arguments) of System T.

Module BI_SystemT <: BI_Struct.

Module Export ST := ST_SystemT.

Module Export BOrd := BOrdWF.

Infix "<B" := lt (at level 70).

Lemma ltB_wf : well_founded lt.

Import SetUtil.

Inductive acc : F -> set nat :=
| Acc_Succ : acc Succ 0.

Definition Acc := acc.

Lemma Acc_arity f i (hi : Acc f i) : i < arity (typ f).

Lemma Acc_ok f i (hi : Acc f i) a :
occurs a (Vnth (inputs (typ f)) (Acc_arity hi)) ->
a <B output_base (typ f)
\/ (a = output_base (typ f)
/\ pos a (Vnth (inputs (typ f)) (Acc_arity hi))).

Notation aeq := (@aeq F X FOrd.eq_dec XOrd.eq_dec ens_X var_notin).
Notation supterm_acc := (@supterm_acc F X So typ Acc Acc_arity).

End BI_SystemT.

CC structure for the termination proof of System T.

Module CC_SystemT <: CC_Struct.

Module Export BI := BI_SystemT.

Notation cc := (@cc F X So ens_X env typ Acc Acc_arity).

End CC_SystemT.

Termination proof of System T.

Module Export SN := SN_rewrite CC_SystemT RS_SystemT DLQO_SystemT.

Import DLQO_SystemT RS_SystemT.

Lemma tr_sn_SystemT : forall E v V, E |- v ~: V -> SN R_aeq v.