Library hydras.Gamma0.Gamma0
A notation system for ordinals less than Gamma0
From Coq Require Import Arith List Lia Compare_dec Relations
Wellfounded RelationClasses.
From hydras Require Import Epsilon0.
From hydras Require Import More_Arith Restriction.
From hydras Require Import ON_Generic.
From hydras Require Import rpo.term rpo.rpo.
From hydras Require Import T2.
From hydras Require Import Compat815.
Import Datatypes.
Set Implicit Arguments.
Lemma nf_a : ∀ a b n c, nf (gcons a b n c) → nf a.
Lemma nf_b : ∀ a b n c, nf (gcons a b n c) → nf b.
Lemma nf_c : ∀ a b n c, nf (gcons a b n c) → nf c.
#[global] Hint Resolve nf_a nf_b nf_c : T2.
Ltac nf_inv := ((eapply nf_a; eassumption)||
(eapply nf_b; eassumption)||
(eapply nf_c; eassumption)).
Lemma zero_lt_succ : ∀ alpha, zero t2< succ alpha.
Lemma not_lt_zero : ∀ alpha, ¬ alpha t2< zero.
Lemma lt_irr : ∀ alpha, ¬ alpha t2< alpha.
Ltac lt_clean :=
try (match goal with
[ineq : lt ?a zero |- _ ] ⇒ case (not_lt_zero ineq);auto
|[ineq : Peano.lt ?a 0 |- _ ] ⇒ case (Nat.nlt_0_r a);auto
|[ref : lt ?a ?a |- _] ⇒ case (lt_irr ref);auto
|[ref : Peano.lt ?a ?a |- _] ⇒ case (lt_irr ref);auto
end).
Lemma le_zero_alpha : ∀ alpha, zero t2≤ alpha.
Lemma psi_le_cons : ∀ alpha beta n gamma,
[alpha, beta] t2≤ gcons alpha beta n gamma.
#[global] Hint Resolve psi_le_cons le_zero_alpha: T2.
Lemma le_psi_term_le alpha beta: alpha t2≤ beta →
psi_term alpha t2≤ psi_term beta.
Lemma le_inv_nc : ∀ a b n c n' c',
gcons a b n c t2≤ gcons a b n' c' → (n<n')%nat ∨ n=n' ∧ c t2≤ c'.
Lemma lt_than_psi : ∀ a b n c a' b',
gcons a b n c t2< [a',b'] →
[a,b]t2<[a',b'].
in order to establish trichotomy, we first use a measure on pair of
terms
Section lemmas_on_length.
Open Scope nat_scope.
Lemma tricho_lt_2 : ∀ a1 a2 b1 b2 n1 n2 r1 r2,
t2_length a1 + t2_length a2 <
t2_length (gcons a1 b1 n1 r1) +
t2_length (gcons a2 b2 n2 r2).
Lemma tricho_lt_2' : ∀ a1 a2 b1 b2 n1 n2 r1 r2,
t2_length b1 + t2_length (gcons a2 b2 0 zero) <
t2_length (gcons a1 b1 n1 r1) +
t2_length (gcons a2 b2 n2 r2).
Lemma tricho_lt_3 : ∀ a1 a2 b1 b2 n1 n2 r1 r2,
t2_length b1 + t2_length b2 <
t2_length (gcons a1 b1 n1 r1) + t2_length (gcons a2 b2 n2 r2).
Lemma tricho_lt_4 : ∀ a1 a2 b1 b2 n1 n2 r1 r2,
t2_length a2 + t2_length a1 <
t2_length (gcons a1 b1 n1 r1) +
t2_length (gcons a2 b2 n2 r2).
Lemma tricho_lt_4' : ∀ a1 a2 b1 b2 n1 n2 c1 c2,
t2_length (gcons a1 b1 0 c1) + t2_length b2 <
t2_length (gcons a1 b1 n1 c1) +
t2_length (gcons a2 b2 n2 c2).
Lemma tricho_lt_5 : ∀ a1 a2 b1 n1 n2 c1 c2,
t2_length a2 + t2_length a1 <
t2_length (gcons a1 b1 n1 c1) +
t2_length (gcons a2 (gcons a1 b1 0 zero) n2 c2).
Lemma tricho_lt_7 : ∀ a1 b1 n1 c1 c2,
t2_length c1 + t2_length c2 <
t2_length (gcons a1 b1 n1 c1) +
t2_length (gcons a1 b1 n1 c2).
End lemmas_on_length.
#[global] Hint Resolve tricho_lt_7 tricho_lt_5 tricho_lt_4 tricho_lt_4' tricho_lt_3 tricho_lt_2 tricho_lt_2 : T2.
Open Scope T2_scope.
Lemma tricho_aux (l: nat) : ∀ t t': T2,
t2_length t + t2_length t' < l →
{t t2< t'} + {t = t'} + {t' t2< t}.
Definition lt_eq_lt_dec (t t': T2) : {t t2< t'}+{t = t'}+{t' t2< t}.
Definition lt_ge_dec : ∀ t t', {t t2< t'}+{t' t2≤ t}.
Defined.
#[ global ] Instance compare_T2 : Compare T2 :=
fun (t1 t2 : T2) ⇒
match lt_eq_lt_dec t1 t2 with
| inleft (left _) ⇒ Lt
| inleft (right _) ⇒ Eq
| inright _ ⇒ Gt
end.
Fixpoint nfb (alpha : T2) : bool :=
match alpha with
zero ⇒ true
| gcons a b n zero ⇒ andb (nfb a) (nfb b)
| gcons a b n ((gcons a' b' n' c') as c) ⇒
match compare [a', b'] [a, b] with
Lt ⇒ andb (nfb a) (andb (nfb b) (nfb c))
| _ ⇒ false
end
end.
Ltac tricho t t' Hname := case (lt_eq_lt_dec t t');
[intros [Hname|Hname] | intro Hname].
Tactic Notation "tricho" constr(t) constr(t') ident(Hname) := tricho t t' Hname.
Section trans_proof.
Variables a1 b1 c1 a2 b2 c2 a3 b3 c3:T2.
Variables n1 n2 n3:nat.
Hypothesis H12 : gcons a1 b1 n1 c1 t2< gcons a2 b2 n2 c2.
Hypothesis H23 : gcons a2 b2 n2 c2 t2< gcons a3 b3 n3 c3.
Hypothesis induc : ∀ t t' t'',
(t2_length t + t2_length t' +
t2_length t'' <
t2_length (gcons a1 b1 n1 c1) +
t2_length (gcons a2 b2 n2 c2) +
t2_length (gcons a3 b3 n3 c3))%nat →
lt t t' → lt t' t'' → lt t t''.
Lemma trans_aux : gcons a1 b1 n1 c1 t2< gcons a3 b3 n3 c3.
End trans_proof.
Lemma lt_trans0 : ∀ n,
∀ t1 t2 t3,
(t2_length t1 + t2_length t2 + t2_length t3 < n)%nat →
lt t1 t2 → lt t2 t3 → lt t1 t3.
Theorem lt_trans :
∀ t1 t2 t3, t1 t2< t2 → t2 t2< t3 → t1 t2< t3.
Theorem le_lt_trans alpha beta gamma: alpha t2≤ beta →
beta t2< gamma →
alpha t2< gamma.
Theorem lt_le_trans alpha beta gamma :
alpha t2< beta → beta t2≤ gamma → alpha t2< gamma.
Theorem le_trans : ∀ alpha beta gamma, alpha t2≤ beta →
beta t2≤ gamma →
alpha t2≤ gamma.
Lemma psi_lt_head : ∀ alpha beta n gamma alpha' beta' n' gamma',
[alpha, beta] t2< [alpha', beta'] →
gcons alpha beta n gamma t2< gcons alpha' beta' n' gamma'.
Lemma nf_inv_tail : ∀ a b n c , nf (gcons a b n c) →
c t2< [a,b].
Theorem lt_beta_psi : ∀ beta alpha, beta t2< [alpha, beta].
Lemma lt_beta_cons : ∀ alpha beta n gamma,
beta t2< gcons alpha beta n gamma.
Theorem lt_alpha_psi : ∀ alpha beta, alpha t2< [alpha, beta].
Lemma lt_alpha_cons : ∀ alpha beta n gamma,
alpha t2< gcons alpha beta n gamma.
#[global] Hint Resolve lt_beta_cons lt_alpha_cons : T2.
Lemma le_cons_tail alpha beta n gamma gamma':
gamma t2≤ gamma' →
gcons alpha beta n gamma t2≤ gcons alpha beta n gamma'.
Lemma nf_fin_inv : ∀ gamma n, nf (gcons zero zero n gamma) →
gamma = zero.
Lemma lt_tail0: ∀ c, nf c → c ≠ zero → gtail c t2< c.
Lemma lt_tail: ∀ a b n c, nf (gcons a b n c) → c t2< gcons a b n c.
Lemma le_one_cons : ∀ a b n c, one t2≤ gcons a b n c.
#[global] Hint Resolve le_one_cons : T2.
Lemma fin_lt_omega : ∀ n, fin n t2< omega.
Lemma omega_lt_epsilon0 : omega t2< epsilon0.
Lemma omega_lt_epsilon : ∀ alpha, omega t2< epsilon alpha.
Lemma lt_one_inv : ∀ alpha, alpha t2< one → alpha = zero.
Lemma lt_cons_omega_inv : ∀ alpha beta n gamma,
gcons alpha beta n gamma t2< omega →
nf (gcons alpha beta n gamma) →
alpha = zero ∧ beta = zero ∧ gamma = zero.
Lemma lt_omega_inv alpha : nf alpha → alpha t2< omega →
{n:nat | alpha = fin n}.
Lemma lt_omega_is_fin alpha: nf alpha → alpha t2< omega →
is_finite alpha.
Theorem lt_compat (n p : nat): fin n t2< fin p →
(n < p)%nat.
Theorem lt_compatR (n p : nat): (n <p)%nat →
fin n t2< fin p.
Lemma finite_is_finite : ∀ n, is_finite (fin n).
Lemma is_finite_finite : ∀ alpha, is_finite alpha →
{n : nat | alpha = fin n}.
Lemma compare_reflect alpha beta : match compare alpha beta with
| Lt ⇒ alpha t2< beta
| Eq ⇒ alpha = beta
| Gt ⇒ beta t2< alpha
end.
Lemma compare_correct alpha beta :
CompareSpec (alpha = beta) (lt alpha beta) (lt beta alpha)
(compare alpha beta).
Lemma compare_Lt : ∀ alpha beta, compare alpha beta = Lt →
alpha t2< beta.
Compare with the proof of T2.Ex6
Example Ex6 : gcons 1 0 12 omega t2< [0,[2,1]].
Lemma compare_Eq : ∀ (alpha beta : T2), compare alpha beta = Eq →
alpha = beta.
Lemma compare_Gt : ∀ alpha beta, compare alpha beta = Gt →
beta t2< alpha.
Arguments compare_Gt [alpha beta].
Arguments compare_Lt [alpha beta].
Arguments compare_Eq [alpha beta].
#[global] Hint Resolve compare_Eq compare_Lt compare_Gt : T2.
Lemma compare_rw_lt alpha beta : alpha t2< beta →
compare alpha beta = Lt.
Lemma compare_rw_eq (alpha beta : T2): alpha = beta →
compare alpha beta = Eq.
Lemma compare_rw_gt alpha beta: beta t2< alpha →
compare alpha beta = Gt.
plus is defined here, because it requires decidable comparison
Fixpoint plus (t1 t2 : T2) {struct t1} : T2 :=
match t1,t2 with
| zero, y ⇒ y
| x, zero ⇒ x
| gcons a b n c, gcons a' b' n' c' ⇒
(match compare (gcons a b 0 zero)
(gcons a' b' 0 zero) with
| Lt ⇒ gcons a' b' n' c'
| Gt ⇒ gcons a b n (c + gcons a' b' n' c')
| Eq ⇒ gcons a b (S(n+n')) c'
end)
end
where "alpha + beta" := (plus alpha beta): T2_scope.
Example Ex7 : 3 + epsilon0 = epsilon0.
Lemma plus_alpha_0 (alpha: T2): alpha + zero = alpha.
Lemma lt_succ (alpha: T2): alpha t2< succ alpha.
Theorem lt_succ_le alpha : ∀ beta, alpha t2< beta → nf beta →
succ alpha t2≤ beta.
Lemma succ_lt_le : ∀ a b, nf a → nf b → a t2< succ b → a t2≤ b.
Lemma succ_of_cons : ∀ a b n c, zero t2< a ∨ zero t2< b →
succ (gcons a b n c)= gcons a b n (succ c).
Inductive subterm : T2 → T2 → Prop :=
| subterm_a : ∀ a b n c, subterm a (gcons a b n c)
| subterm_b : ∀ a b n c, subterm b (gcons a b n c)
| subterm_c : ∀ a b n c, subterm c (gcons a b n c)
| subterm_trans : ∀ t t1 t2, subterm t t1 → subterm t1 t2 →
subterm t t2.
Lemma nf_subterm alpha beta : subterm alpha beta →
nf beta → nf alpha.
Theorem subterm_lt alpha beta: subterm alpha beta → nf beta →
alpha t2< beta.
Ltac subtermtac :=
match goal with
[|- subterm ?t1 (gcons ?t1 ?t2 ?n ?t3)] ⇒
constructor 1
| [|- subterm ?t2 (gcons ?t1 ?t2 ?n ?t3)] ⇒
constructor 2
| [|- subterm ?t3 (gcons ?t1 ?t2 ?n ?t3)] ⇒
constructor 3
| [|- subterm ?t4 (gcons ?t1 ?t2 ?n ?t3)] ⇒
((constructor 4 with t1; subtermtac) ||
(constructor 4 with t2; subtermtac) ||
(constructor 4 with t3; subtermtac))
end.
Module Gamma0_sig <: Signature.
Inductive symb0 : Set := nat_0 | nat_S | ord_zero | ord_psi | ord_cons.
Definition symb := symb0.
Lemma eq_symbol_dec : ∀ f1 f2 : symb, {f1 = f2} + {f1 ≠ f2}.
The arity of a symbol contains also the information about built-in theories as in CiME
Inductive arity_type : Set :=
| AC : arity_type
| C : arity_type
| Free : nat → arity_type.
Definition arity : symb → arity_type :=
fun f ⇒ match f with
| nat_0 ⇒ Free 0
| ord_zero ⇒ Free 0
| nat_S ⇒ Free 1
| ord_psi ⇒ Free 2
| ord_cons ⇒ Free 3
end.
End Gamma0_sig.
Module Vars <: Variables.
Inductive empty_set : Set := .
Definition var := empty_set.
Lemma eq_variable_dec : ∀ v1 v2 : var, {v1 = v2} + {v1 ≠ v2}.
End Vars.
Module Gamma0_prec <: Precedence.
Definition A : Set := Gamma0_sig.symb.
Import Gamma0_sig.
Definition prec : relation A :=
fun f g ⇒ match f, g with
| nat_0, nat_S ⇒ True
| nat_0, ord_zero ⇒ True
| nat_0, ord_cons ⇒ True
| nat_0, ord_psi ⇒ True
| ord_zero, nat_S ⇒ True
| ord_zero, ord_cons ⇒ True
| ord_zero, ord_psi ⇒ True
| nat_S, ord_cons ⇒ True
| nat_S, ord_psi ⇒ True
| ord_cons, ord_psi ⇒ True
| _, _ ⇒ False
end.
Inductive status_type : Set :=
| Lex : status_type
| Mul : status_type.
Definition status : A → status_type := fun f ⇒ Lex.
Lemma prec_dec : ∀ a1 a2 : A, {prec a1 a2} + {¬ prec a1 a2}.
Lemma prec_antisym : ∀ s, prec s s → False.
Lemma prec_transitive : transitive prec.
End Gamma0_prec.
Module Gamma0_alg <: Term := term.Make (Gamma0_sig) (Vars).
Module Gamma0_rpo <: RPO := rpo.Make (Gamma0_alg) (Gamma0_prec).
Import Gamma0_alg Gamma0_rpo Gamma0_sig.
Fixpoint nat_2_term (n:nat) : term :=
match n with 0 ⇒ (Term nat_0 nil)
| S p ⇒ Term nat_S ((nat_2_term p)::nil)
end.
Lemma nat_lt_cons : ∀ (n:nat) t p c ,
rpo (nat_2_term n)
(Term ord_cons (t::p::c::nil)).
Lemma nat_lt_psi : ∀ (n:nat) a b, rpo (nat_2_term n)
(Term ord_psi (a::b::nil)).
Theorem rpo_trans : ∀ t t1 t2, rpo t t1 → rpo t1 t2 → rpo t t2.
Fixpoint T2_2_term (a:T2) : term :=
match a with
zero ⇒ Term ord_zero nil
|gcons a b 0 zero ⇒ Term ord_psi (T2_2_term a :: T2_2_term b ::nil)
|gcons a b n c ⇒
Term ord_cons (Term ord_psi
(T2_2_term a :: T2_2_term b ::nil) ::nat_2_term n ::
T2_2_term c::nil)
end.
Fixpoint T2_size (o:T2):nat :=
match o with zero ⇒ 0
| gcons a b n c ⇒ S (T2_size a + T2_size b + n + T2_size c)%nat
end.
Lemma T2_size1 : ∀ a b n c, (T2_size zero < T2_size (gcons a b n c))%nat.
Lemma T2_size2 : ∀ a b n c , (T2_size a < T2_size (gcons a b n c))%nat.
Lemma T2_size3 : ∀ a b n c , (T2_size b < T2_size (gcons a b n c))%nat.
Lemma T2_size4 : ∀ a b n c , (T2_size c < T2_size (gcons a b n c))%nat.
#[global] Hint Resolve T2_size1 T2_size2 T2_size3 T2_size4 : T2.
let us recall subterm properties on T2
Lemma lt_subterm1 : ∀ a a' n' b' c', a t2< a' →
a t2< gcons a' b' n' c'.
#[global] Hint Resolve nat_lt_cons lt_subterm1 : T2.
Lemma nat_2_term_mono : ∀ n n', (n < n')%nat →
rpo (nat_2_term n) (nat_2_term n').
Lemma T2_size_psi : ∀ a b n c ,
(T2_size [a,b] ≤ T2_size (gcons a b n c))%nat.
Lemma rpo_2_2 : ∀ ta1 ta2 tb1 tb2 ,
rpo ta1 ta2 →
rpo tb1 (Term ord_psi (ta2:: tb2::nil)) →
rpo (Term ord_psi (ta1:: tb1 ::nil))
(Term ord_psi (ta2:: tb2 ::nil)).
Lemma rpo_2_3 : ∀ ta1 ta2 tb1 tb2 n1 tc1,
rpo ta1 ta2 →
rpo tb1 (Term ord_psi (ta2:: tb2::nil)) →
rpo tc1 (Term ord_psi (ta1:: tb1::nil)) →
rpo (Term ord_cons ((Term ord_psi (ta1:: tb1 ::nil))
::(nat_2_term n1)::tc1::nil))
(Term ord_psi (ta2:: tb2 ::nil)).
Lemma rpo_2_1 : ∀ ta1 ta2 tb1 tb2 n1 n2 tc1 tc2,
rpo ta1 ta2 →
rpo tb1 (Term ord_psi (ta2:: tb2::nil)) →
rpo tc1 (Term ord_psi (ta1:: tb1::nil)) →
rpo (Term ord_cons
((Term ord_psi (ta1:: tb1 ::nil))::(nat_2_term n1) ::tc1::nil))
(Term ord_cons ((Term ord_psi (ta2:: tb2 ::nil))
::(nat_2_term n2) ::tc2::nil)).
Lemma rpo_2_4 : ∀ ta1 ta2 tb1 tb2 n2 tc2,
rpo ta1 ta2 →
rpo tb1 (Term ord_psi (ta2:: tb2::nil)) →
rpo (Term ord_psi (ta1:: tb1 ::nil))
(Term ord_cons
((Term ord_psi
(ta2:: tb2 ::nil)):: (nat_2_term n2) ::tc2::nil)).
Lemma rpo_3_2 : ∀ ta1 tb1 tb2 ,
rpo tb1 tb2 →
rpo (Term ord_psi (ta1:: tb1 ::nil))
(Term ord_psi (ta1:: tb2 ::nil)).
Lemma rpo_3_3 : ∀ ta1 tb1 tb2 n1 tc1,
rpo tb1 tb2 →
rpo tc1 (Term ord_psi (ta1:: tb1 ::nil)) →
rpo (Term ord_cons
((Term ord_psi (ta1:: tb1 ::nil))::(nat_2_term n1) ::tc1::nil))
(Term ord_psi (ta1:: tb2 ::nil)).
Lemma rpo_3_1 : ∀ ta1 tb1 tb2 n1 n2 tc1 tc2,
rpo tb1 tb2 →
rpo tc1 (Term ord_psi (ta1:: tb1::nil)) →
rpo (Term ord_cons
((Term ord_psi (ta1:: tb1 ::nil))::(nat_2_term n1) ::tc1::nil))
(Term ord_cons
((Term ord_psi (ta1:: tb2 ::nil))::(nat_2_term n2) ::tc2::nil)).
Lemma rpo_3_4 : ∀ ta1 tb1 tb2 n2 tc2,
rpo tb1 tb2 →
rpo (Term ord_psi (ta1:: tb1 ::nil))
(Term ord_cons
((Term ord_psi (ta1:: tb2 ::nil))::
(nat_2_term n2) ::tc2::nil)).
Lemma rpo_4_2 : ∀ ta1 ta2 tb1 tb2 ,
rpo (Term ord_psi (ta1:: tb1 ::nil)) tb2 →
rpo (Term ord_psi (ta1:: tb1 ::nil))
(Term ord_psi (ta2:: tb2 ::nil)).
Lemma rpo_4_3 : ∀ ta1 ta2 tb1 tb2 n1 tc1,
rpo (Term ord_psi (ta1:: tb1 ::nil)) tb2 →
rpo tc1 (Term ord_psi (ta1:: tb1 ::nil)) →
rpo (Term ord_cons
((Term ord_psi (ta1:: tb1 ::nil))::
(nat_2_term n1) ::tc1::nil))
(Term ord_psi (ta2:: tb2 ::nil)).
Lemma rpo_4_1 : ∀ ta1 ta2 tb1 tb2 n1 n2 tc1 tc2,
rpo (Term ord_psi (ta1:: tb1 ::nil)) tb2 →
rpo tc1 (Term ord_psi (ta1:: tb1 ::nil)) →
rpo
(Term ord_cons
((Term ord_psi (ta1:: tb1 ::nil))::
(nat_2_term n1) ::tc1::nil))
(Term ord_cons
((Term ord_psi (ta2:: tb2 ::nil))::
(nat_2_term n2) ::tc2::nil)).
Lemma rpo_4_4 : ∀ ta1 ta2 tb1 tb2 n2 tc2,
rpo (Term ord_psi (ta1:: tb1 ::nil)) tb2 →
rpo (Term ord_psi (ta1:: tb1 ::nil))
(Term ord_cons
((Term ord_psi (ta2:: tb2 ::nil))::
(nat_2_term n2) ::tc2::nil)).
Lemma rpo_5_2 :
∀ ta1 ta2 tb1 ,
rpo (Term ord_psi (ta1:: tb1 ::nil))
(Term ord_psi (ta2:: (Term ord_psi (ta1::tb1::nil)) ::nil)).
Lemma rpo_5_3 : ∀ ta1 ta2 tb1 n1 tc1,
rpo tc1 (Term ord_psi (ta1:: tb1 ::nil)) →
rpo
(Term ord_cons
((Term ord_psi (ta1:: tb1 ::nil))::
(nat_2_term n1) ::tc1::nil))
(Term ord_psi (ta2:: (Term ord_psi (ta1:: tb1 ::nil)) ::nil)).
Lemma rpo_5_1 : ∀ ta1 ta2 tb1 n1 n2 tc1 tc2,
rpo tc1 (Term ord_psi (ta1:: tb1 ::nil)) →
rpo
(Term ord_cons
((Term ord_psi (ta1:: tb1 ::nil))::
(nat_2_term n1) ::tc1::nil))
(Term ord_cons
((Term ord_psi (ta2::
(Term ord_psi (ta1:: tb1 ::nil))
::nil))::
(nat_2_term n2) ::tc2::nil)).
Lemma rpo_5_4 : ∀ ta1 ta2 tb1 n2 tc2,
rpo (Term ord_psi (ta1:: tb1 ::nil))
(Term ord_cons
((Term ord_psi (ta2::
(Term ord_psi (ta1:: tb1 ::nil))
::nil))::
(nat_2_term n2) ::tc2::nil)).
Lemma rpo_6_1 : ∀ ta1 tb1 n1 n2 tc1 tc2,
rpo tc1 (Term ord_psi (ta1:: tb1 ::nil)) →
(n1 < n2)%nat →
rpo
(Term ord_cons
((Term ord_psi (ta1:: tb1 ::nil))::
(nat_2_term n1) ::tc1::nil))
(Term ord_cons
((Term ord_psi (ta1:: tb1 ::nil)):: (nat_2_term n2) ::tc2::nil)).
Lemma rpo_6_4 : ∀ ta1 tb1 n2 tc2,
(0 < n2)%nat →
rpo (Term ord_psi (ta1:: tb1 ::nil))
(Term ord_cons
((Term ord_psi (ta1:: tb1 ::nil))::
(nat_2_term n2) ::tc2::nil)).
Lemma rpo_7_1 : ∀ ta1 tb1 n1 tc1 tc2,
rpo tc1 (Term ord_psi (ta1:: tb1 ::nil)) →
rpo tc1 tc2 →
rpo (Term ord_cons
((Term ord_psi (ta1:: tb1 ::nil))::
(nat_2_term n1) ::tc1::nil))
(Term ord_cons
((Term ord_psi (ta1:: tb1 ::nil))::
(nat_2_term n1) ::tc2::nil)).
Section lt_incl_rpo.
Variable s :nat.
Variables (a1 b1 c1 a2 b2 c2:T2)(n1 n2:nat).
Hypothesis Hsize :
((T2_size (gcons a1 b1 n1 c1) + T2_size (gcons a2 b2 n2 c2)) = S s)%nat.
Hypothesis Hrec : ∀ o' o, (T2_size o + T2_size o' ≤ s)%nat→
o t2< o' → nf o → nf o' →
rpo (T2_2_term o) (T2_2_term o').
Hypothesis nf1 : nf (gcons a1 b1 n1 c1).
Hypothesis nf2 : nf (gcons a2 b2 n2 c2).
Remark nf_a1 : nf a1.
Remark nf_a2 : nf a2.
Remark nf_b1 : nf b1.
Remark nf_b2 : nf b2.
#[local] Hint Resolve nf1 nf2 nf_a1 nf_a2 nf_b1 nf_b2 : T2.
Remark nf_c1 : nf c1.
Remark nf_c2 : nf c2.
#[local] Hint Resolve nf_c1 nf_c2 : T2.
Hypothesis H : gcons a1 b1 n1 c1 t2< gcons a2 b2 n2 c2.
Lemma cons_rw : ∀ a b n c,
(n=0 ∧ c=zero ∧
(T2_2_term (gcons a b n c)=
(Term ord_psi
((T2_2_term a)::(T2_2_term b)::nil)))) ∨
(T2_2_term (gcons a b n c)=
Term ord_cons
((Term ord_psi ((T2_2_term a)::(T2_2_term b)::nil))
::(nat_2_term n)::(T2_2_term c)::nil)).
Lemma lt_rpo_cons_cons : rpo (T2_2_term (gcons a1 b1 n1 c1))
(T2_2_term (gcons a2 b2 n2 c2)).
End lt_incl_rpo.
Lemma lt_inc_rpo_0 : ∀ n,
∀ o' o, (T2_size o + T2_size o' ≤ n)%nat→
o t2< o' → nf o → nf o' →
rpo (T2_2_term o) (T2_2_term o').
Remark R1 : Acc P.prec nat_0.
#[global] Hint Resolve R1 : T2.
Remark R2 : Acc P.prec ord_zero.
#[global] Hint Resolve R2 : T2.
Remark R3 : Acc P.prec nat_S.
#[global] Hint Resolve R3 : T2.
Remark R4 : Acc P.prec ord_cons.
#[global] Hint Resolve R4 : T2.
Remark R5 : Acc P.prec ord_psi.
#[global] Hint Resolve R5 : T2.
Theorem well_founded_rpo : well_founded rpo.
Section well_founded.
Let R := restrict nf lt.
#[local] Hint Unfold restrict R : T2.
Lemma R_inc_rpo : ∀ o o', R o o' → rpo (T2_2_term o) (T2_2_term o').
Lemma nf_Wf : well_founded_restriction _ nf lt.
End well_founded.
Definition transfinite_induction :
∀ (P:T2 → Type),
(∀ x:T2, nf x →
(∀ y:T2, nf y → y t2< x → P y) → P x) →
∀ a, nf a → P a.
Definition transfinite_induction_Q :
∀ (P : T2 → Type) (Q : T2 → Prop),
(∀ x:T2, Q x → nf x →
(∀ y:T2, Q y → nf y → y t2< x → P y) → P x) →
∀ a, nf a → Q a → P a.
Definition phi (alpha beta : T2) : T2 :=
match beta with
zero ⇒ [alpha, beta]
| [b1, b2] ⇒
(match compare alpha b1
with Datatypes.Lt ⇒ [b1, b2 ]
| _ ⇒ [alpha,[b1, b2]]
end)
| gcons b1 b2 0 (gcons zero zero n zero) ⇒
(match compare alpha b1
with Datatypes.Lt ⇒
[alpha, (gcons b1 b2 0 (fin n))]
| _ ⇒ [alpha, (gcons b1 b2 0 (fin (S n)))]
end)
| any_beta ⇒ [alpha, any_beta]
end.
Example Ex8: phi 1 (succ epsilon0) = [1, [1,0] + 1].
All epsilons are fixpoints of phi 0
Theorem epsilon_fxp : ∀ beta, phi zero (epsilon beta) =
epsilon beta.
Theorem epsilon0_fxp : epsilon0 = phi zero epsilon0.
Theorem phi_of_psi : ∀ a b1 b2,
phi a [b1, b2] =
if (lt_ge_dec a b1)
then [b1, b2]
else [a ,[b1, b2]].
Lemma phi_to_psi : ∀ alpha beta,
{alpha' : T2 & {beta' : T2 | phi alpha beta = [alpha', beta']}}.
Lemma phi_principal : ∀ alpha beta, ap (phi alpha beta).
Theorem phi_alpha_zero : ∀ alpha, phi alpha zero = [alpha, zero].
Theorem phi_of_psi_succ : ∀ a b1 b2 n,
phi a (gcons b1 b2 0 (fin (S n))) =
if lt_ge_dec a b1
then [a, (gcons b1 b2 0 (fin n))]
else [a ,(gcons b1 b2 0 (fin (S n)))].
Lemma phi_cases_aux : ∀ P : T2 → Type,
P zero →
(∀ b1 b2, nf b1 → nf b2 → P [b1, b2]) →
(∀ b1 b2 n, nf b1 → nf b2 →
P (gcons b1 b2 0 (fin (S n)))) →
(∀ b1 b2 n c, nf (gcons b1 b2 n c) →
omega t2≤ c ∨ (0 < n)%nat →
P (gcons b1 b2 n c)) →
∀ alpha, nf alpha → P alpha.
Theorem phi_cases' :
∀ a b, nf b →
{b1 :T2 & {b2:T2 | b = [b1, b2] ∧
a t2< b1 ∧ phi a b = b}} +
{phi a b = [a, b]} +
{b1 :T2 & {b2:T2 &
{n: nat | b = gcons b1 b2 0 (fin (S n)) ∧
a t2< b1 ∧
phi a b =
[a, (gcons b1 b2 0 (fin n))]}}}.
Theorem phi_cases : ∀ a b, nf b →
{phi a b = b} +
{phi a b = [a, b]} +
{b': T2 | nf b' ∧ phi a b = [a, b']
∧ succ b' = b}.
Theorem phi_nf : ∀ alpha beta, nf alpha →
nf beta →
nf (phi alpha beta).
Lemma phi_of_any_cons : ∀ alpha beta1 beta2 n gamma,
omega t2≤ gamma ∨ (0 < n)%nat →
phi alpha (gcons beta1 beta2 n gamma) =
[alpha, (gcons beta1 beta2 n gamma)].
Lemma phi_fix alpha beta :
phi alpha beta = beta →
{beta1 : T2 & {beta2 : T2 | beta = [beta1, beta2]
∧ alpha t2< beta1}}.
Lemma phi_le : ∀ alpha beta alpha' beta',
nf beta →
phi alpha beta = [alpha', beta'] → alpha t2≤ alpha'.
Lemma phi_le_ge :
∀ alpha beta, nf alpha → nf beta →
{alpha':T2 &
{beta':T2
| phi alpha beta = [alpha' ,beta'] ∧
alpha t2≤ alpha' ∧
beta' t2≤ beta}}.
phi alpha beta is a common fixpoint of all the phi gamma,
for any gamma t2< alpha as specified by Schutte
Theorem phi_spec1 : ∀ alpha beta gamma,
nf alpha → nf beta → nf gamma →
gamma t2< alpha →
phi gamma (phi alpha beta) = phi alpha beta.
Theorem phi_principalR alpha beta :
nf alpha → nf beta →
{gamma:T2 | [alpha, beta] = phi zero gamma}.
Lemma phi_alpha_zero_gt_alpha : ∀ alpha, alpha t2< phi alpha zero.
Theorem le_b_phi_ab : ∀ a b, nf a → nf b → b t2≤ phi a b.
Lemma phi_of_psi_plus_fin : ∀ a b1 b2 n,
a t2< b1 → phi a (gcons b1 b2 0 (fin n)) t2<
[a ,gcons b1 b2 0 (fin n)].
Lemma phi_mono_r : ∀ a b c, nf a → nf b → nf c →
b t2< c → phi a b t2< phi a c.
Lemma phi_mono_weak_r : ∀ a b c, nf a → nf b → nf c →
b t2≤ c → phi a b t2≤ phi a c.
Lemma phi_inj_r : ∀ a b c, nf a → nf b → nf c →
phi a b = phi a c → b = c.
Lemma lt_a_phi_ab : ∀ a b, nf a → nf b → a t2< phi a b.
Lemma zero_not_lim : ¬ is_limit zero.
Lemma F_not_lim : ∀ n, ¬ is_limit (fin n).
Lemma succb_not_lim alpha: is_successor alpha → ¬ is_limit alpha.
Lemma is_limit_not_succ alpha: is_limit alpha → ¬ is_successor alpha.
limit_plus_fin alpha n beta means :
beta = alpha + fin n and (alpha is limit or alpha = zero)
Inductive limit_plus_fin : T2 → nat → T2 → Prop :=
limit_plus_F_0 : ∀ p, limit_plus_fin zero p (fin p)
|limit_plus_F_cons : ∀ beta1 beta2 n gamma0 gamma p,
zero t2< beta1 ∨ zero t2< beta2 →
limit_plus_fin gamma0 p gamma →
limit_plus_fin (gcons beta1 beta2 n gamma0)
p (gcons beta1 beta2 n gamma).
Lemma limit_plus_fin_plus : ∀ alpha alpha' p,
limit_plus_fin alpha p alpha' →
nf alpha →
alpha' = alpha + fin p.
Lemma limit_plus_fin_lim : ∀ alpha alpha' p,
limit_plus_fin alpha p alpha' →
nf alpha →
is_limit alpha ∨ alpha=zero.
Lemma limit_plus_fin_inv0 alpha beta:
limit_plus_fin alpha 0 beta →
nf alpha → alpha = beta.
Lemma is_limit_cons_inv : ∀ b1 b2 n c, nf (gcons b1 b2 n c) →
is_limit (gcons b1 b2 n c) → is_limit c ∨ c = zero.
Lemma is_limit_intro : ∀ b1 b2 n , nf b1 → nf b2 →
zero t2< b1 ∨ zero t2< b2 →
is_limit (gcons b1 b2 n zero).
Lemma lt_epsilon0_ok : ∀ alpha, nf alpha → lt_epsilon0 alpha →
alpha t2< epsilon0.
Derive Inversion_clear lt_01 with (∀ (a b:T2),
gcons a b 0 zero t2< epsilon0) Sort Prop.
Derive Inversion_clear lt_02 with (∀ (a b c:T2)(n:nat),
gcons a b n c t2< epsilon0) Sort Prop.
Lemma psi_lt_epsilon0 : ∀ a b, [a, b] t2< epsilon0 →
a = zero ∧ b t2< epsilon0.
Lemma cons_lt_epsilon0 : ∀ a b n c, gcons a b n c t2< epsilon0 →
nf (gcons a b n c) →
a = zero ∧ b t2< epsilon0 ∧ c t2< epsilon0.
Lemma lt_epsilon0_okR: ∀ alpha, nf alpha → alpha t2< epsilon0 →
lt_epsilon0 alpha.
Lemma T1_to_T2_inj : ∀ alpha beta : T1,
T1_to_T2 alpha = T1_to_T2 beta → alpha = beta.
Lemma T1_to_T2_lt : ∀ c, lt_epsilon0 (T1_to_T2 c).
Definition T1_to_T2_R : ∀ a, lt_epsilon0 a → {c:T1 | T1_to_T2 c = a}.
Lemma T1_to_T2_mono : ∀ alpha beta, T1.lt alpha beta →
T1_to_T2 alpha t2< T1_to_T2 beta.
Lemma T1_to_T2_monoR : ∀ c c', lt (T1_to_T2 c) (T1_to_T2 c') → T1.lt c c'.
Lemma lt_epsilon0_trans : ∀ a, lt_epsilon0 a → nf a →
∀ b, lt b a → nf b → lt_epsilon0 b.
Lemma nf_coeff_irrelevance : ∀ a b n n' c, nf (gcons a b n c) →
nf (gcons a b n' c).
Lemma psi_principal : ∀ a b c d, nf c → c t2< [a, b]
→ d t2< [a, b] →
c + d t2< [a, b].
Lemma nf_intro : ∀ a b n c, nf a → nf b →
c t2< [a,b ] → nf c → nf (gcons a b n c).
Lemma plus_nf : ∀ alpha, nf alpha → ∀ beta, nf beta →
nf (alpha + beta).
Lemma succ_as_plus : ∀ alpha, nf alpha → alpha + one = succ alpha.
Lemma succ_nf : ∀ alpha, nf alpha → nf (succ alpha).
Lemma lt_epsilon0_succ : ∀ a, lt_epsilon0 a → lt_epsilon0 (succ a).
Check epsilon0.
Theorem epsilon0_as_lub : ∀ b, nf b →
(∀ a, lt_epsilon0 a → lt a b) →
le epsilon0 b.
Locate epsilon0.
Definition lub (P: T2 → Prop)(x:T2) :=
nf x ∧
(∀ y, P y → nf y → y t2≤ x) ∧
(∀ y, (∀ x, P x → nf x → x t2≤ y) → nf y →
x t2≤ y).
Theorem lub_unicity : ∀ P l l', lub P l → lub P l' → l = l'.
Theorem lub_mono : ∀ (P Q :T2 → Prop) l l',
(∀ o, nf o → P o → Q o) →
lub P l → lub Q l' → l t2≤ l'.
Lemma succ_limit_dec : ∀ a, nf a →
{a = zero} +{is_successor a}+{is_limit a}.
Lemma le_plus_r : ∀ alpha beta, nf alpha → nf beta →
alpha t2≤ alpha + beta.
Lemma le_plus_l : ∀ alpha beta, nf alpha → nf beta →
alpha t2≤ beta + alpha.
Lemma plus_mono_r : ∀ alpha , nf alpha → ∀ beta gamma, nf beta →
nf gamma → beta t2< gamma → alpha + beta t2< alpha + gamma.
Lemma plus_mono_l_weak:
∀ o, nf o →
∀ alpha, nf alpha → alpha t2< o →
∀ beta,
nf beta → beta t2< o →
∀ gamma , nf gamma →
alpha t2< beta →
alpha + gamma t2≤ beta + gamma.
Remark R_pred_Sn : ∀ n, pred (fin (S n)) = Some (fin n).
Lemma pred_of_cons : ∀ a b n c,
zero t2< a ∨ zero t2< b →
pred (gcons a b n c) = match pred c with
Some c' ⇒
Some (gcons a b n c')
| None ⇒ None
end.
Lemma pred_of_cons' : ∀ a b n ,
zero t2< a ∨ zero t2< b →
pred (gcons a b n zero) = None.
Lemma is_limit_ab : ∀ alpha beta n gamma,
is_limit (gcons alpha beta n gamma)
→ zero t2< alpha ∨ zero t2< beta.
Lemma pred_of_limit : ∀ alpha,
is_limit alpha → nf alpha → pred alpha = None.
Lemma pred_of_succ : ∀ alpha, nf alpha →
pred (succ alpha) = Some alpha.
Lemma limit_plus_fin_ok : ∀ alpha, is_limit alpha →
∀ n, limit_plus_fin alpha n (alpha + fin n).
Section phi_to_psi.
Variable alpha : T2.
Lemma phi_to_psi_1 : ∀ beta1 beta2 n,
alpha t2< beta1 →
[alpha, (gcons beta1 beta2 0 (fin n))] =
phi alpha (gcons beta1 beta2 0 (fin (S n))).
Lemma phi_to_psi_2 : ∀ beta1 beta2 n,
beta1 t2≤ alpha →
[alpha, (gcons beta1 beta2 0 (fin n))] =
phi alpha (gcons beta1 beta2 0 (fin n)).
Lemma phi_to_psi_3 : ∀ beta1 beta2 ,
beta1 t2≤ alpha →
[alpha, [beta1, beta2]] =
phi alpha [beta1, beta2].
Lemma phi_to_psi_4 : [alpha, zero] = phi alpha zero.
Lemma phi_to_psi_5 :
∀ beta1 beta2 n gamma, omega t2≤ gamma ∨ (0 < n)%nat →
[alpha,gcons beta1 beta2 n gamma] =
phi alpha (gcons beta1 beta2 n gamma).
Lemma phi_to_psi_6 : ∀ beta, nf beta →
phi alpha beta = beta →
[alpha, beta] = phi alpha (succ beta).
Lemma phi_psi : ∀ beta gamma n,
nf gamma →
limit_plus_fin beta n gamma →
phi alpha beta = beta →
[alpha, gamma] = phi alpha (succ gamma).
Theorem th_14_5 : ∀ alpha1 beta1 alpha2 beta2,
nf alpha1 → nf beta1 → nf alpha2 → nf beta2 →
phi alpha1 beta1 = phi alpha2 beta2 →
{alpha1 t2< alpha2 ∧ beta1 = phi alpha2 beta2} +
{alpha1 = alpha2 ∧ beta1 = beta2} +
{alpha2 t2< alpha1 ∧ phi alpha1 beta1 = beta2}.
Lemma lt_not_gt : ∀ a b, a t2< b → ¬ (b t2< a).
Lemma phi_mono_RR : ∀ a b c, nf a → nf b → nf c →
phi a b t2< phi a c → b t2< c.
Theorem th_14_6 : ∀ alpha1 beta1 alpha2 beta2,
nf alpha1 → nf beta1 → nf alpha2 → nf beta2 →
phi alpha1 beta1 t2< phi alpha2 beta2 →
{alpha1 t2< alpha2 ∧ beta1 t2< phi alpha2 beta2} +
{alpha1 = alpha2 ∧ beta1 t2< beta2} +
{alpha2 t2< alpha1 ∧ phi alpha1 beta1 t2< beta2}.
Definition moser_lepper (beta0 beta:T2)(n:nat) :=
limit_plus_fin beta0 n beta ∧ phi alpha beta0 = beta0.
Lemma ml_psi : ∀ beta0 beta n,
moser_lepper beta0 beta n →
{t1 : T2 & {t2: T2| beta0 =
[t1,t2] ∧ alpha t2< t1}}.
Lemma ml_1 : ∀ beta0 beta n, moser_lepper beta0 beta n →
nf beta → nf beta0 →
[alpha, beta] = phi alpha (succ beta).
End phi_to_psi.
Example Ex9 : [zero, epsilon 2 + 4] = phi 0 (epsilon 2 + 5).
Example Ex10 : phi omega [epsilon0, 5] = [epsilon0, 5].
Declare Scope g0_scope.
Module G0.
Definition LT := restrict nf lt.
Lemma Lt_wf : well_founded LT.
Lemma zero_nfb : nfb zero.
Lemma nfb_a a b n c: nfb (gcons a b n c) → nfb a.
Lemma nfb_equiv gamma : nfb gamma = true ↔ nf gamma.
Lemma nfb_proof_unicity :
∀ (alpha:T2) (H H': nfb alpha), H = H'.
Class G0 := mkg0 {vnf : T2; vnf_ok : nfb vnf}.
Definition lt (alpha beta : G0) := T2.lt (@vnf alpha) (@vnf beta).
#[ global ] Instance compare_G0 : Compare G0 :=
fun alpha beta ⇒ compare (@vnf alpha) (@vnf beta).
Lemma lt_LT_incl alpha beta : lt alpha beta → LT (@vnf alpha) (@vnf beta).
#[ global ] Instance lt_sto : StrictOrder lt.
Lemma lt_wf : well_founded lt.
Lemma compare_correct alpha beta :
CompareSpec (alpha = beta) (lt alpha beta) (lt beta alpha)
(compare alpha beta).
#[ global, program ] Instance zero : G0 := @mkg0 T2.zero _.
#[ global, program] Instance Omega : G0 := @mkg0 omega _.
Notation omega := Omega.
Definition le := clos_refl G0 lt.
#[ global ] Instance Gamma0_comp: Comparable lt compare.
#[ global ] Instance Gamma0: ON lt compare.
#[ global ] Instance Finite (n:nat) : G0.
#[ global ] Instance Plus (alpha beta : G0) : G0.
Infix "+" := Plus : g0_scope.
#[ global ] Instance Phi (alpha beta : G0) : G0.
Notation phi := Phi.
Notation phi0 := (Phi zero).
Notation "'omega^'" := phi0 (only parsing) : g0_scope.
Coercion Finite : nat >-> G0.
#[local] Open Scope g0_scope.
Example Ex42 : omega + 42 + omega^ 2 = omega^ 2.
End G0.