Library orden_term
Require Export Termes_tes.
Require Export Wellfounded.
Require Export Wf_nat.
Inductive Ttm : term -> term -> Prop :=
| Ttm_car : (n1,n2:nat)(u1,u2:term)(lt n1 n2)->
(length u1)=(length u2)->
(Ttm (cons n1 u1)(cons n2 u2))
| Ttm_cdr : (n:nat)(u1,u2:term)(Ttm u1 u2)->
(Ttm (cons n u1)(cons n u2)).
Hints Resolve Ttm_car Ttm_cdr.
Lemma Ttm_shorter: (x,y:term)(Ttm x y)->(le (length x) (length y)).
Induction 1; Intros.
Simpl.
Elim H1; Auto.
Simpl.
Auto with v62.
Save.
Lemma list_indlg: (A:Set)(P:(list A)->Prop)
((n:nat)
((v:(list A))(lt (length v) n) -> (P v))
-> (v:(list A))(length v)=n -> (P v))
->(v:(list A))(P v).
Intros.
Cut (n:nat)(v:(list A))(lt (length v) n)->(P v).
Intros.
Apply H0 with (S (length v)); Auto.
Induction n; Intros.
Inversion H0.
(Apply H with (length v0); Intros; Trivial).
Apply H0.
Omega.
Save.
Lemma Ttm_wf : (well_founded ? Ttm).
Red; Intros.
Elim a using list_indlg.
Destruct v; Simpl; Intros.
Constructor; Intros.
Inversion H1.
Cut (lt (length l) n).
Generalize l.
Clear H0 l.
ElimType (Acc ? lt n0).
Intros.
Generalize H2.
ElimType (Acc ? Ttm l); Intros.
Constructor; Intros.
Inversion_clear H6.
Apply H1; Trivial.
Rewrite H8; Trivial.
Apply H4; Trivial.
Apply le_lt_trans with (length x0); Trivial.
Apply Ttm_shorter; Trivial.
Apply H; Trivial.
Apply lt_wf.
Elim H0; Auto.
Save.
Hints Resolve Ttm_wf.
Lemma Ttm_trans: (t1,t2:term)
(Ttm t1 t2)
->(n:nat)
(full n t1)
->(full n t2)
->(t3:term)(full n t3)->(Ttm t2 t3)->(Ttm t1 t3).
Induction 1; Intros.
Generalize H0 H4.
Inversion H5; Intros.
Rewrite H10 in H1.
Constructor 1; Trivial.
Apply lt_trans with n2; Auto.
Constructor 1; Trivial.
Transitivity (pred n).
Cut (full (pred n) u1).
Auto.
Apply full_S with n1:=n1; Auto.
Cut (full (pred n) u3).
Auto.
Apply full_S with n1:=n2; Auto.
Generalize H0 H4.
Inversion H5; Intros.
Generalize H8.
Constructor 1; Trivial.
Transitivity (length u2); Trivial.
Transitivity (pred n0).
Cut (full (pred n0) u1).
Auto.
Apply full_S with n1:=n1; Auto.
Cut (full (pred n0) u2).
Auto.
Apply full_S with n1:=n2; Auto.
Constructor 2.
Apply H1 with n:=(pred n0) t3:=u3; Trivial.
Apply full_S with n1:=n; Auto.
Apply full_S with n1:=n; Auto.
Apply full_S with n1:=n; Auto.
Save.
Hints Resolve Ttm_trans.
Lemma Ttm_antisym : (t1,t2:term)(n:nat)(full n t1)->(full n t2)->
~((Ttm t1 t2)/\(Ttm t2 t1)).
Intros.
Red; Intros.
Elim H1; Intros.
Clear H1.
Generalize t1 t2 n H H0 H2 H3.
Clear H3 H2 H0 H n t2 t1.
Induction 3; Intros.
Inversion H4.
Omega.
Rewrite H8 in H1.
Omega.
Inversion H4.
Omega.
Apply H3; Trivial.
Save.
Hints Resolve Ttm_antisym.
Lemma Ttm_nonrefl: (t:term)~(Ttm t t).
Induction t; Intros.
Red; Intro.
Inversion H.
Red; Intro.
Inversion H0.
Omega.
Elim H; Trivial.
Save.
Hints Resolve Ttm_nonrefl.
Lemma Ttm_strict : (t1,t2:term)(n:nat)(full n t1)->(full n t2)->
(Ttm t1 t2)->~t1=t2.
Red; Intros.
Rewrite H2 in H1.
Apply (Ttm_nonrefl t2); Trivial.
Save.
Hints Resolve Ttm_strict.
Lemma Ttm_total_good: (t1,t2:term)
(n:nat){(full n t1)->(full n t2)->(Ttm t1 t2)}+{(full n t1)->(full n t2)->(Ttm t2 t1)}+{(full n t1)->(full n t2)->t1=t2}.
Induction t1; Induction t2; Intros.
Right; Auto.
Left; Left; Intros.
Inversion H0.
Inversion H1.
Cut (length (nil nat))=(length (cons a l)); Intros.
Elim H4.
Inversion H4.
Transitivity n; Auto.
Left; Right; Intros.
Inversion H0.
Inversion H1.
Cut (length (nil nat))=(length (cons a l)); Intros.
Elim H4.
Inversion H4.
Transitivity n; Auto.
Elim (lt_eq_lt_dec a a0); Intros.
Elim a1; Intros; Clear a1.
Left.
Left; Intros.
Apply Ttm_car; Trivial.
Transitivity (pred n).
Inversion H1; Auto.
Inversion H2; Auto.
Elim H with l0 (pred n); Intros.
Elim a1; Intros; Clear a1.
Left.
Left; Intros.
Rewrite b.
Apply Ttm_cdr.
Apply a2.
Inversion H1; Auto.
Inversion H2; Auto.
Left; Right; Intros.
Rewrite b.
Apply Ttm_cdr.
Apply b0.
Inversion H1; Auto.
Inversion H2; Auto.
Right; Intros.
Rewrite b.
Replace l0 with l; Trivial.
Apply b0.
Inversion H1; Auto.
Inversion H2; Auto.
Left.
Right; Intros.
Apply Ttm_car; Trivial.
Transitivity (pred n).
Inversion H2; Auto.
Inversion H1; Auto.
Save.
Hints Resolve Ttm_total_good.
Lemma Ttm_total : (t1,t2:term)(n:nat)(full n t1)->(full n t2)->
{Ttm t1 t2}+{Ttm t2 t1}+{t1 = t2}.
Intros.
Elim Ttm_total_good with t1 t2 n; Intros.
Elim a; Intros.
Left; Auto.
Left; Right; Auto.
Right; Auto.
Save.
Hints Resolve Ttm_total.
Lemma ord_adm1: (n:nat)(t:term)(full n t)->(~t=(n_term_O n))->
(Ttm (n_term_O n) t).
Induction n.
Induction t; Intros.
Simpl in H0.
Elim H0; Trivial.
Simpl.
Auto.
Inversion H0.
Induction t; Intros.
Inversion H0.
Simpl.
(Elim (zerop a); Intros).
Rewrite a0.
Apply Ttm_cdr.
(Apply H; Auto).
(Red; Intros).
Red in H2.
Apply H2.
Rewrite a0.
(Rewrite H3; Auto).
(Apply Ttm_car; Trivial).
(Cut (full n0 l); Intros; Auto).
Red in H3.
(Rewrite H3; Trivial).
Save.
Hints Resolve ord_adm1.
Lemma Ttm_a2: (t,u:term)(n:nat)(full n t)->(full n u)->
(Ttm t u)->(v:term)(full n v)->(Ttm (term_mult t v) (term_mult u v)).
Induction t.
Induction u; Intros.
Cut ~(Ttm (nil nat) (nil nat)); Auto; Intros.
Elim H3; Auto.
Inversion H0.
Inversion H1.
Cut (length (nil nat))=(length (cons a l)); Intros.
Elim H6.
Inversion H6.
Transitivity n; Auto.
Induction u.
Intros.
Inversion H2.
Induction v; Auto; Intros.
Simpl.
Inversion H3.
Apply Ttm_car.
Omega.
Cut (full (pred n) (term_mult l l1)); Intros.
Cut (full (pred n) (term_mult l0 l1)); Intros.
Inversion H12.
Inversion H13.
Transitivity (pred n); Auto.
Cut (full (pred n) l0); Intros.
Cut (full (pred n) l1); Auto.
Inversion H5; Auto.
Inversion H2; Auto.
Cut (full (pred n) l); Intros.
Cut (full (pred n) l1); Auto.
Inversion H5; Auto.
Inversion H1; Auto.
Apply Ttm_cdr.
Apply H with n:=(pred n); Trivial.
Inversion H1; Auto.
Inversion H2; Auto.
Inversion H5; Auto.
Save.
Hints Resolve Ttm_a2.
Lemma mon_term_mult: (t,u:term)(n:nat)(full n t)->(full n u)->
(Ttm t u)->(v:term)(full n v)->(Ttm (term_mult v t) (term_mult v u)).
Intros.
Replace (term_mult v t) with (term_mult t v); Auto.
Replace (term_mult v u) with (term_mult u v); Auto.
Apply Ttm_a2 with n:=n; Auto.
Save.
Hints Resolve mon_term_mult.
Index
This page has been generated by coqdoc