Library Lcm_tes
Require Export divisib_tes.
Definition max_num: nat->nat->nat:=
[n,m:nat]Cases (le_gt_dec n m) of
(left _) => m
| (right _) => n
end.
Hints Unfold max_num.
Lemma max_num1: (n1,n2:nat)(le n1 n2)->((max_num n1 n2) = n2).
(Unfold max_num; Intros).
(Elim (le_gt_dec n1 n2); Auto).
(Intros; Omega).
Save.
Hints Resolve max_num1.
Lemma max_num2: (n,n1:nat)(le n1 n)->(n2:nat)(le n2 n)->
(le (max_num n1 n2) n).
Unfold max_num; Intros.
(Elim (le_gt_dec n1 n2); Auto).
Save.
Hints Resolve max_num2.
Lemma max_numO: (n:nat)((max_num n O)=n).
Unfold max_num; Intros.
(Elim (le_gt_dec n O); Auto).
(Intros; Omega).
Save.
Hints Resolve max_numO.
Lemma max_num_conm: (n1,n2:nat)((max_num n1 n2) = (max_num n2 n1)).
(Unfold max_num; Intros).
(Elim (le_gt_dec n1 n2); Elim (le_gt_dec n2 n1)).
(Intros; Omega).
Auto.
Auto.
(Intros; Omega).
Save.
Hints Resolve max_num_conm.
Fixpoint lcm [t1,t2:term]: term:=
Cases t1 t2 of
nil nil => (nil ?)
|nil (cons y z) => (cons y z)
|(cons y z) nil => (cons y z)
|(cons n1 t1') (cons n2 t2') => (cons (max_num n1 n2) (lcm t1' t2'))
end.
Lemma lcm_full: (n:nat)(t1:term)(t2:term)(full n t1)->(full n t2)->
(full n (lcm t1 t2)).
Unfold full; Induction n.
Induction t1; Induction t2; Trivial.
Intros; Simpl.
Inversion H1.
Intros.
Generalize H0 H1.
Case t1; Case t2; Simpl; Auto.
Save.
Hints Resolve lcm_full.
Lemma lcm_conm: (t,t':term)((lcm t t')=(lcm t' t)).
Induction t; Induction t'; Intros; Auto.
Simpl.
Replace (max_num a a0) with (max_num a0 a); Auto.
Save.
Hints Resolve lcm_conm.
Lemma div_lcm1: (t1,t2:term)(term_div t1 (lcm t1 t2)).
Induction t1; Auto.
Induction t2; Intros; Auto.
Simpl.
Apply term_div_cons; Trivial.
Unfold max_num.
Elim (le_gt_dec a a0); Trivial.
Save.
Hints Resolve div_lcm1.
Lemma div_lcm2: (t1,t2:term)(term_div t2 (lcm t1 t2)).
Intros.
Replace (lcm t1 t2) with (lcm t2 t1); Auto.
Save.
Hints Resolve div_lcm2.
Lemma lcm_1: (t:term)(n:nat)(full n t)->
((lcm t (n_term_O n)) = t).
Induction t; Intros.
Inversion H; Auto.
Inversion H0.
Simpl.
Replace (max_num a O) with a; Auto.
Save.
Hints Resolve lcm_1.
Lemma lcm_2: (t:term)(n:nat)(full n t)->
((lcm (n_term_O n) t) = t).
Intros.
(Transitivity (lcm t (n_term_O n)); Auto).
Save.
Hints Resolve lcm_2.
Lemma lcm_div2: (t1,t2:term)(term_div t1 t2)->
(n:nat)(full n t1)->(full n t2)->((lcm t1 t2) = t2).
Induction 1; Intros.
Rewrite -> (nterm_null t H0 n H1); Auto.
Simpl.
Replace (lcm t t') with t'.
Replace (max_num n1 n2) with n2; Auto.
Symmetry; Auto.
Red in H3 H4.
Symmetry.
Rewrite <- H4 in H3.
Simpl in H3.
Apply H2 with (length t); Auto.
Save.
Hints Resolve lcm_div2.
Lemma lcm_div: (t1,t2:term)(term_div t1 t2)->
(t3:term)(term_div t3 t2)->(n:nat)(full n t1)->(full n t2)->
(full n t3)->(term_div (lcm t1 t3) t2).
Induction 1.
Intros.
Rewrite -> (nterm_null t H0 n H2).
Rewrite -> lcm_2; Trivial.
Induction t3; Intros.
Simpl.
Constructor 2; Trivial.
Simpl.
Constructor 2.
Inversion H4; Auto.
Inversion H8.
Replace (max_num n1 O) with n1; Auto.
Elim H2 with l (pred n).
Auto.
Auto.
Inversion H4; Trivial.
Inversion H8; Auto.
Inversion H5; Auto.
Inversion H6; Auto.
Inversion H7; Auto.
Save.
Hints Resolve lcm_div.
Index
This page has been generated by coqdoc