Library divisib_tes
Require Export orden_term.
Inductive term_div: term->term->Prop :=
term_div_null : (t:term)(t':term)(null_term t)->(term_div t t')
| term_div_cons: (n1,n2:nat)(t,t':term)(le n1 n2)->(term_div t t')->
(term_div (cons n1 t) (cons n2 t')).
Hints Resolve term_div_null term_div_cons.
Lemma null_div: (t1,t2:term)(term_div t1 t2)->(null_term t2)->(null_term t1).
(Induction 1; Intros; Auto).
Generalize H0.
(Inversion_clear H3; Intros).
(Replace n1 with O; Auto).
Omega.
Save.
Hints Resolve null_div.
Lemma div_trans: (t1,t2:term)(term_div t1 t2)->(t3:term)(term_div t2 t3)->
(term_div t1 t3).
Induction 1; Intros; Auto.
Inversion H3; Intros.
Inversion H4.
Constructor 1.
Replace n1 with O.
Constructor 2.
Apply null_div with t'; Auto.
Omega.
Constructor 2; EAuto.
Apply le_trans with n2; Auto.
Save.
Hints Resolve div_trans.
Lemma term_div_n_eq: (t:term)(term_div t t).
(Induction t; Auto).
Save.
Hints Resolve term_div_n_eq.
Lemma term_div_n_comp: (t1,t2:term)(term_div t1 t2)->
(t:term)(term_div t1 (term_mult t t2)).
Induction 1; Intros; Auto.
Case t0; Intros.
Simpl; Auto.
Simpl; Apply term_div_cons.
Replace (plus n n2) with (plus n2 n); Omega.
Apply H2.
Save.
Hints Resolve term_div_n_comp.
Lemma term_mult_div : (t1,t2:term)
(term_div t1 (term_mult t1 t2)).
Intros.
Replace (term_mult t1 t2) with (term_mult t2 t1);Auto.
Save.
Hints Resolve term_mult_div.
Lemma dec_term_div: (t1,t2:term)(n:nat)(full n t1)->(full n t2)->
{(term_div t1 t2)} + {~(term_div t1 t2)}.
Induction t1.
Intros.
Left; Auto.
Induction t2; Intros.
Elim (eq_tm_dec (cons a l) (nil nat)); Intros.
Left.
Rewrite a0; Auto.
Right.
Inversion H1.
Simpl in H2.
Inversion H0.
Simpl in H3.
Rewrite <- H2 in H3.
Cut ~(S (length l))=(0); Intros.
Elim H4; Auto.
Omega.
Cut (full (pred n) l); Intros.
Cut (full (pred n) l0); Intros.
Elim (lt_eq_lt_dec a a0); Intros.
Elim a1; Intros; Clear a1.
Elim H with l0 (pred n); Intros; Trivial.
Left.
Constructor 2; Auto.
Omega.
Right.
Red; Intros.
Inversion H5; Auto.
Inversion H6; Auto.
Elim H with l0 (pred n); Intros; Trivial.
Left.
Rewrite b.
Constructor 2; Auto.
Right.
Red; Intros.
Rewrite b in H5.
Inversion H5; Auto.
Inversion H6; Auto.
Right.
Red; Intros.
Inversion H5.
Cut a=O; Intros.
Rewrite H9 in b.
Omega.
Inversion H6; Auto.
Omega.
Inversion H2; Auto.
Inversion H1; Auto.
Save.
Fixpoint div_term [t1,t2:term]: term:=
Cases t1 t2 of
nil x => x | x nil => x
| (cons n1 t1') (cons n2 t2') =>
(cons (minus n1 n2) (div_term t1' t2'))
end.
Lemma term_div_full: (n:nat)(t1:term)(t2:term)(full n t1)->
(full n t2)->(full n (div_term t1 t2)).
Unfold full; Induction n.
Induction t1; Induction t2; Trivial.
Intros; Simpl.
Inversion H1.
Intros n0 H t1 t2.
Case t1; Case t2; Simpl; Intros; Trivial.
Case t1; Case t2; Simpl; Intros; Auto.
Save.
Hints Resolve term_div_full.
Lemma term_div_full_S:(n,n1,n2:nat)(t,t':term)
(full n (cons n1 t))->(full n (cons n2 t'))->
(full n (cons (minus n2 n1) (div_term t' t))).
Induction n; Intros.
Inversion H.
Apply full_pred1; Auto.
Save.
Hints Resolve term_div_full_S.
Lemma term_div_eq:(t:term)(n:nat)(full n t)->((div_term t t)=(n_term_O n)).
Induction t; Intros; Auto.
Inversion H0; Simpl.
Replace (minus a a) with O.
Auto.
Omega.
Save.
Hints Resolve term_div_eq.
Lemma term_div_full_nulo : (t:term)(n:nat)(full n t)->
((div_term t (n_term_O n)) = t).
Induction t; Intros.
Inversion H; Auto.
Inversion H0; Simpl.
Replace (minus a O) with a.
Auto.
Omega.
Save.
Hints Resolve term_div_full_nulo.
Lemma mult_div_term1: (t,t1:term)(term_div t t1)->
(n:nat) (full n t)->(full n t1)->(t2:term)(full n t2)->
((term_mult (div_term t1 t) t2) =
(div_term (term_mult t1 t2) t)).
Induction 1.
Intros.
Rewrite -> (nterm_null t0 H0 n H1).
Rewrite -> term_div_full_nulo; Trivial.
Rewrite -> term_div_full_nulo; Auto.
Destruct t2; Simpl; Intros; Trivial.
Generalize H3 H4 H5 .
Case n; Intros.
Inversion H8.
Elim H2 with n3 l; Auto.
Replace (plus (minus n2 n1) n0) with (minus (plus n2 n0) n1).
Auto.
Omega.
Save.
Hints Resolve mult_div_term1.
Lemma divis_im_divt: (u1,u2:term)(term_div u1 u2)->
(n:nat)(full n u1)->(full n u2)->
(u2=(term_mult u1 (div_term u2 u1))).
Intros.
Transitivity (term_mult (div_term u2 u1) u1); Auto.
Transitivity (div_term (term_mult u2 u1) u1).
Transitivity (term_mult (div_term u1 u1) u2).
Replace (div_term u1 u1) with (n_term_O n).
Transitivity (term_mult u2 (n_term_O n)); Auto.
Symmetry; Auto.
Symmetry; Auto.
Replace (term_mult u2 u1) with (term_mult u1 u2); Auto.
Apply mult_div_term1 with n; Auto.
Symmetry.
Apply mult_div_term1 with n; Auto.
Save.
Hints Resolve divis_im_divt.
Lemma eg_denom_term: (t,t1,t2:term)(t1 = t2)->
((div_term t1 t) = (div_term t2 t)).
Intros.
(Rewrite -> H; Auto).
Save.
Hints Resolve eg_denom_term.
Lemma div_mult_mon_inv: (t1,t2:term)(n:nat)(full n t1)->(full n t2)
->(div_term (term_mult t2 t1) t2)=t1.
Intros.
Transitivity (term_mult (div_term t2 t2) t1).
Symmetry.
Apply mult_div_term1 with n; Auto.
Transitivity (term_mult (n_term_O n) t1); Auto.
Transitivity (term_mult t1 (n_term_O n)); Auto.
Save.
Hints Resolve div_mult_mon_inv.
Lemma simpl_term: (t,t',t1:term)(n:nat)(full n t)->
(full n t')->(full n t1)->
(term_div t' t1)->(term_div t1 t)->
(div_term t t')=
(term_mult (div_term t1 t') (div_term t t1)).
Intros.
Transitivity (term_mult (div_term t t') (n_term_O n)).
Symmetry; Auto.
Transitivity (term_mult (div_term t t') (div_term t1 t1)).
Transitivity (term_mult (n_term_O n) (div_term t t')); Auto.
Transitivity (term_mult (div_term t1 t1) (div_term t t')); Auto.
Apply term_mult_r.
Symmetry; Auto.
Transitivity (div_term (term_mult t (div_term t1 t1)) t').
Apply mult_div_term1 with n; Auto.
Apply div_trans with t1; Trivial.
Transitivity (div_term (term_mult t1 (div_term t t1)) t').
Apply eg_denom_term.
Transitivity t.
Symmetry.
Transitivity (term_mult t (n_term_O n)).
Symmetry; Auto.
Transitivity (term_mult (n_term_O n) t); Auto.
Transitivity (term_mult (div_term t1 t1) t); Auto.
Apply term_mult_r.
Symmetry; Auto.
Apply divis_im_divt with n; Auto.
Symmetry.
Apply mult_div_term1 with n; Auto.
Save.
Hints Resolve simpl_term.
Lemma ex_term_div_n: (t1,t2:term)(term_div t1 t2)->
(n:nat)(full n t1)->(full n t2)->
(Ex [t3:term]((full n t3) /\ (t2 = (term_mult t1 t3)))).
Intros.
Split with (div_term t2 t1).
Split; Auto.
Apply divis_im_divt with n; Auto.
Save.
Hints Resolve ex_term_div_n.
Lemma comp_divis_lex: (t1,t2:term)(term_div t1 t2)->
(n:nat)(full n t1)->(full n t2)->(Ttm t1 t2)\/(t1=t2).
Intros.
Elim ex_term_div_n with t1 t2 n; Intros; Trivial.
Elim H2; Intros.
Clear H2.
Elim eq_tm_dec with t1 t2; Intros.
Right; Trivial.
Left.
Elim eq_tm_dec with (n_term_O n) x; Intros.
Rewrite <- a in H4.
Cut t1=(term_mult t1 (n_term_O n)); Intros.
Rewrite <- H4 in H2.
Elim b; Auto.
Symmetry; Apply term_mult_full_nulo; Auto.
Cut (Ttm (n_term_O n) x); Intros; Auto.
Replace t1 with (term_mult t1 (n_term_O n)); Auto.
Rewrite H4.
Apply mon_term_mult with n; Auto.
Save.
Hints Resolve comp_divis_lex.
Index
This page has been generated by coqdoc