Library Termes_tes
Require Export Peano_dec.
Require Export Arith.
Require Export PolyList.
Require Export Omega.
Require Export PolyListSyntax.
Definition term:= (list nat).
Hints Unfold term.
Definition full:= [n:nat][t:term]((length t) = n).
Hints Unfold full.
Lemma S_imp_eq: (n,n':nat)((S n)=(S n'))->(n=n').
Auto.
Save.
Hints Resolve S_imp_eq.
Lemma nat_S_p:(n:nat)(lt O n)->((S (pred n)) = n).
Induction 1; Auto.
Save.
Hints Resolve nat_S_p.
Lemma full_S: (n,n1:nat)(t:term)(full n (cons n1 t))->
(full (pred n) t).
Induction 1; Auto.
Save.
Hints Resolve full_S.
Lemma full_pred1: (n:nat)(t:term)(full n t)->
(n1:nat)(full (S n) (cons n1 t)).
Induction n.
Intros.
(Inversion H; Auto).
Intros.
(Inversion H0; Auto).
Save.
Hints Resolve full_pred1.
Inductive null_term: term -> Prop:=
null_term_nil: (null_term (nil ?))
|null_term_cons: (t:term)(null_term t)->(null_term (cons O t)).
Hints Resolve null_term_nil null_term_cons.
Fixpoint n_term_O [n:nat]: term:=
Cases n of
O => (nil ?)
|(S n) => (cons O (n_term_O n))
end.
Lemma length_n_term_O: (n:nat)(length (n_term_O n))=n.
Induction n; Auto; Intros.
Simpl.
Rewrite H; Auto.
Save.
Hints Resolve length_n_term_O.
Lemma null_term_term_O: (n:nat)(null_term (n_term_O n)).
(Induction n; Auto).
Intros.
Simpl.
(Apply null_term_cons; Auto).
Save.
Hints Resolve null_term_term_O.
Theorem full_O : (n:nat)(full n (n_term_O n)).
(Induction n; Auto).
Save.
Hints Resolve full_O.
Lemma nterm_null:
(t:term)(null_term t)->(n:nat)(full n t)->t=(n_term_O n).
(Induction 1; Simpl; Intros).
(Inversion_clear H0; Auto).
Inversion H2.
Simpl.
Simpl in H3.
Pattern 1 t0 .
(Rewrite -> (H1 (length t0)); Auto).
Save.
Hints Resolve nterm_null.
Fixpoint term_mult [t1,t2:term]: term:=
Cases t1 t2 of
nil x => x
| x nil => x
| (cons n1 t1') (cons n2 t2') =>
(cons (plus n1 n2) (term_mult t1' t2'))
end.
Theorem term_mult_conmt: (t,t':term)((term_mult t t') = (term_mult t' t)).
(Induction t; Induction t'; Auto).
Intros.
Simpl.
Replace (plus a a0) with (plus a0 a).
Replace (term_mult l l0) with (term_mult l0 l); Auto.
Omega.
Save.
Hints Resolve term_mult_conmt.
Theorem term_mult_assoc: (t,t1,t2:term)
((term_mult (term_mult t t1) t2) = (term_mult t (term_mult t1 t2))).
(Induction t; Induction t1; Induction t2; Auto).
Intros.
Simpl.
Replace (plus (plus a a0) a1) with (plus a (plus a0 a1)).
(Replace (term_mult (term_mult l l0) l1)
with (term_mult l (term_mult l0 l1)); Auto).
Omega.
Save.
Hints Resolve term_mult_assoc.
Lemma term_mult_r: (t,t1,t2:term)(t1 = t2)->
((term_mult t1 t) = (term_mult t2 t)).
Induction 1;Auto.
Save.
Hints Resolve term_mult_r.
Lemma term_mult_perm: (t,t1,t2:term)((term_mult (term_mult t t1) t2) =
(term_mult t1 (term_mult t t2))).
Intros.
Replace (term_mult (term_mult t t1) t2) with
(term_mult (term_mult t1 t) t2); Auto.
Save.
Hints Resolve term_mult_perm.
Theorem term_mult_full_nulo: (t:term)(n:nat)(full n t)->
((term_mult t (n_term_O n)) = t).
Induction t.
Intros.
Inversion H.
Auto.
Intros.
Inversion H0.
Simpl.
(Replace (plus a O) with a; Auto).
(Replace (term_mult l (n_term_O (length l))) with l; Auto).
Symmetry.
Apply H.
Auto.
Save.
Hints Resolve term_mult_full_nulo.
Lemma term_mult_full: (t1:term)(t2:term)(n:nat)(full n t1)->
(full n t2)->(full n (term_mult t1 t2)).
Unfold full.
(Induction t1; Simpl; Intros).
Elim H0.
Simpl.
(Case t2; Simpl; Auto).
Generalize H1 .
(Case t2; Simpl; Intros; Auto).
(Rewrite -> (H l0 (length l0)); Auto).
(Cut (S (length l))=(S (length l0)); Auto).
(Rewrite -> H2; Auto).
Save.
Hints Resolve term_mult_full.
Lemma eqterm_cons1: (t1,t2:term)(n1:nat)(t1 = t2)->
((cons n1 t1) = (cons n1 t2)).
Intros.
(Rewrite -> H; Auto).
Save.
Hints Resolve eqterm_cons1.
Lemma eqexp_cons: (t:term)(n1,n2:nat)(n1 = n2)->
((cons n1 t) = (cons n2 t)).
Intros.
(Rewrite -> H; Auto).
Save.
Hints Resolve eqexp_cons.
Lemma eq_tm_dec : (t1,t2:term){t1=t2}+{~(t1=t2)}.
Induction t1.
Induction t2.
Left; Trivial.
Intros a t22 HR; Right.
Discriminate.
Intros a u hru ; Induction t2.
Right; Discriminate.
Intros b v hrv.
Elim (eq_nat_dec a b); Intros He.
Elim (hru v); Intros Ht.
Left; Rewrite He; Rewrite Ht; Auto.
Right; Unfold not; Intros HH; Apply Ht; Injection HH; Auto.
Right; Unfold not; Intros HH; Apply He; Injection HH; Auto.
Save.
Hints Resolve eq_tm_dec.
Lemma term_mult_can_full: (t,t',t0:term)(n:nat)(full n t)-> (full n t')->(term_mult t0 t)=(term_mult t0 t')-> t=t'. Induction t; Destruct t'; Intros; Auto.
Inversion H.
Inversion H0.
Rewrite <- H3 in H2.
Inversion H2.
Inversion H1.
Inversion H0.
Rewrite <- H4 in H3.
Inversion H3.
Generalize H2.
Elim t0; Auto.
Intros.
Simpl in H4.
Injection H4.
Intros.
Replace a with n.
Replace l0 with l; Auto.
(Apply H with t':=l0 t0:=l1 n:=(pred n0); Trivial).
Inversion H0; Auto.
Inversion H1; Auto.
Apply simpl_plus_l with n:=a0; Auto.
Save.
Hints Resolve term_mult_can_full.
Lemma term_mult_n_eq: (t,t',t0:term)(n:nat)(full n t)->
(full n t')->(~(t=t'))->
(~((term_mult t0 t)=(term_mult t0 t'))).
Intros.
(Red; Intros).
Elim H1.
(Apply term_mult_can_full with t0:=t0 n:=n; Auto).
Save.
Hints Resolve term_mult_n_eq.
Index
This page has been generated by coqdoc