X is the set of variables, it has to come with a decidable equality
syntax of terms
Inductive T: Set :=
| dot: T -> T -> T
| pls: T -> T -> T
| opp: T -> T
| one: T
| zer: T
| var: X -> T.
| dot: T -> T -> T
| pls: T -> T -> T
| opp: T -> T
| one: T
| zer: T
| var: X -> T.
notations
Notation "x + y" := (pls x y) (at level 50, left associativity): U_scope.
Notation "x * y" := (dot x y) (at level 40, left associativity): U_scope.
Notation "- x" := (opp x): U_scope.
Notation "1" := (one): U_scope.
Notation "0" := (zer): U_scope.
Notation "x * y" := (dot x y) (at level 40, left associativity): U_scope.
Notation "- x" := (opp x): U_scope.
Notation "1" := (one): U_scope.
Notation "0" := (zer): U_scope.
Definition monom := list X.
Definition polynom := list (Z * monom).
Notation lex e f := (match e with Eq => f | _ => e end).
Fixpoint monom_compare (m n: monom) :=
match m,n with
| [],[] => Eq
| [],_ => Lt
| _ ,[] => Gt
| x::m,y::n => lex (nat_compare x y) (monom_compare m n)
end.
Lemma monom_compare_wspec: forall n m, CompSpec eq (fun _ _ => True) n m (monom_compare n m).
Definition readm (m: monom): T := fold_right (fun x q => var x * q) 1 m.
Fixpoint copy t p :=
match p with
| xH => t
| xO p => copy t p+copy t p
| xI p => copy t p+copy t p+t
end.
Definition readzm zm :=
let '(z,m) := zm in
match z with
| Z0 => 0
| Zpos p => copy (readm m) p
| Zneg p => - copy (readm m) p
end.
Definition read (p: polynom): T := fold_right (fun zm q => readzm zm + q) 0 p.
Definition poly_one: polynom := [(1%Z,[])].
Definition poly_zer: polynom := [].
Definition poly_var i: polynom := [(1%Z,[i])].
Definition poly_opp (p: polynom): polynom :=
map (fun zm => let '(z,m) := zm in (Zopp z,m)) p.
Definition zm z m p: polynom := if Z_eq_dec z 0 then p else (z,m)::p.
Fixpoint poly_pls p: polynom -> polynom :=
match p with
| [] => fun q => q
| (x,m)::p' =>
let fix poly_pls_aux q :=
match q with
| [] => p
| (y,n)::q' =>
match monom_compare m n with
| Eq => zm (x+y) m (poly_pls p' q')
| Lt => (x,m)::poly_pls p' q
| Gt => (y,n)::poly_pls_aux q'
end
end
in poly_pls_aux
end.
Fixpoint insert x m (p: polynom): polynom :=
match p with
| [] => [(x,m)]
| (y,n)::p' =>
match monom_compare m n with
| Eq => zm (x+y) m p'
| Lt => (x,m)::p
| Gt => (y,n)::insert x m p'
end
end.
Definition rdot y n: polynom -> polynom := map (fun xm => let '(x,m) := xm in (Zmult x y,m++n)).
Definition ldot x m: polynom -> polynom := map (fun yn => let '(y,n) := yn in (Zmult x y,m++n)).
Fixpoint poly_dot (p q: polynom): polynom :=
match p,q with
| [],_ => poly_zer
| _,[] => poly_zer
| (x,m)::p', (y,n)::q' =>
poly_pls (poly_pls (insert
(x*y) (m++n)
(rdot y n p'))
(ldot x m q'))
(poly_dot p' q')
end.
Fixpoint eval (t: T): polynom :=
match t with
| x+y => poly_pls (eval x) (eval y)
| x*y => poly_dot (eval x) (eval y)
| -x => poly_opp (eval x)
| 1 => poly_one
| 0 => poly_zer
| var i => poly_var i
end.
I is the set of pretypes, s and t give the typing environment (source and target)
typing judgement
Inductive typed: I -> I -> T -> Prop :=
| t_var: forall x, typed (s x) (t x) (var x)
| t_one: forall n, typed n n 1
| t_zer: forall n m, typed n m 0
| t_dot: forall n m o u v, typed n m u -> typed m o v -> typed n o (u*v)
| t_pls: forall n m u v, typed n m u -> typed n m v -> typed n m (u+v)
| t_opp: forall n m u, typed n m u -> typed n m (-u).
| t_var: forall x, typed (s x) (t x) (var x)
| t_one: forall n, typed n n 1
| t_zer: forall n m, typed n m 0
| t_dot: forall n m o u v, typed n m u -> typed m o v -> typed n o (u*v)
| t_pls: forall n m u v, typed n m u -> typed n m v -> typed n m (u+v)
| t_opp: forall n m u, typed n m u -> typed n m (-u).
typed equality judgement
Inductive equal: I -> I -> relation T :=
| vrefl: forall x, equal (s x) (t x) (var x) (var x)
| orefl: forall n, equal n n 1 1
| zrefl: forall n m, equal n m 0 0
| dot_assoc: forall u v w n m o p, typed n m u -> typed m o v -> typed o p w -> equal n p (u*(v*w)) ((u*v)*w)
| one_dot: forall u n m, typed n m u -> equal n m (1*u) u
| dot_one: forall u n m, typed n m u -> equal n m (u*1) u
| zer_dot: forall u n m o, typed n m u -> equal o m (0*u) 0
| dot_zer: forall u n m o, typed n m u -> equal n o (u*0) 0
| pls_dot: forall u v w n m o, typed n m u -> typed o n v -> typed o n w -> equal o m ((v+w)*u) (v*u+w*u)
| dot_pls: forall u v w n m o, typed n m u -> typed m o v -> typed m o w -> equal n o (u*(v+w)) (u*v+u*w)
| pls_assoc: forall u v w n m, typed n m u -> typed n m v -> typed n m w -> equal n m (u+(v+w)) ((u+v)+w)
| zer_pls: forall u n m, typed n m u -> equal n m (0+u) u
| pls_comm: forall u v n m, typed n m u -> typed n m v -> equal n m (u+v) (v+u)
| pls_opp: forall u n m, typed n m u -> equal n m (u+-u) 0
| dot_compat: forall n m p, Proper (equal n m ==> equal m p ==> equal n p) dot
| pls_compat: forall n m, Proper (equal n m ==> equal n m ==> equal n m) pls
| opp_compat: forall n m, Proper (equal n m ==> equal n m) opp
| trans: forall n m, Transitive (equal n m)
| sym: forall n m, Symmetric (equal n m).
| vrefl: forall x, equal (s x) (t x) (var x) (var x)
| orefl: forall n, equal n n 1 1
| zrefl: forall n m, equal n m 0 0
| dot_assoc: forall u v w n m o p, typed n m u -> typed m o v -> typed o p w -> equal n p (u*(v*w)) ((u*v)*w)
| one_dot: forall u n m, typed n m u -> equal n m (1*u) u
| dot_one: forall u n m, typed n m u -> equal n m (u*1) u
| zer_dot: forall u n m o, typed n m u -> equal o m (0*u) 0
| dot_zer: forall u n m o, typed n m u -> equal n o (u*0) 0
| pls_dot: forall u v w n m o, typed n m u -> typed o n v -> typed o n w -> equal o m ((v+w)*u) (v*u+w*u)
| dot_pls: forall u v w n m o, typed n m u -> typed m o v -> typed m o w -> equal n o (u*(v+w)) (u*v+u*w)
| pls_assoc: forall u v w n m, typed n m u -> typed n m v -> typed n m w -> equal n m (u+(v+w)) ((u+v)+w)
| zer_pls: forall u n m, typed n m u -> equal n m (0+u) u
| pls_comm: forall u v n m, typed n m u -> typed n m v -> equal n m (u+v) (v+u)
| pls_opp: forall u n m, typed n m u -> equal n m (u+-u) 0
| dot_compat: forall n m p, Proper (equal n m ==> equal m p ==> equal n p) dot
| pls_compat: forall n m, Proper (equal n m ==> equal n m ==> equal n m) pls
| opp_compat: forall n m, Proper (equal n m ==> equal n m) opp
| trans: forall n m, Transitive (equal n m)
| sym: forall n m, Symmetric (equal n m).
sanity requirements
Lemma equal_refl: forall n m u, typed n m u -> equal n m u u.
Lemma equal_typed: forall n m u v, equal n m u v -> typed n m u /\ typed n m v.
we need those lines to circumvent a bug with setoid_rewrite
derived typed equalities
Lemma pls_zer: forall u n m, typed n m u -> equal n m (u+0) u.
Lemma opp_zer: forall n m, equal n m (-0) 0.
Lemma equal_pls: forall w n m u v, equal n m (u+w) (v+w) -> equal n m u v.
Lemma opp_pls: forall n m u v, typed n m u -> typed n m v -> equal n m (-(u+v)) ((-u)+(-v)).
Lemma opp_invol: forall u n m, typed n m u -> equal n m (--u) u.
Lemma opp_dot_l: forall n m p a b, typed n m a -> typed m p b -> equal n p (-a*b) (-(a*b)).
Lemma opp_dot_r: forall n m p a b, typed n m a -> typed m p b -> equal n p (a*-b) (-(a*b)).
Lemma opp_dot: forall n m p a b, typed n m a -> typed m p b -> equal n p (-a*-b) (a*b).
Inductive mtyped: I -> I -> monom -> Prop :=
| mt_nil: forall n, mtyped n n []
| mt_cons: forall n x q, mtyped (t x) n q -> mtyped (s x) n (x::q).
Inductive ptyped: I -> I -> polynom -> Prop :=
| pt_nil: forall n m, ptyped n m []
| pt_cons: forall n m z x q, mtyped n m x -> ptyped n m q -> ptyped n m ((z,x)::q).
Lemma copy_typed: forall n m p, typed n m p -> forall z, typed n m (copy p z).
Lemma readm_typed: forall n m p, mtyped n m p -> typed n m (readm p).
Lemma readzm_typed: forall n m z x, mtyped n m x -> typed n m (readzm (z,x)).
Lemma read_typed: forall n m p, ptyped n m p -> typed n m (read p).
Lemma opp_ptyped: forall n m u, ptyped n m u -> ptyped n m (poly_opp u).
Lemma pls_ptyped: forall n m u, ptyped n m u -> forall v, ptyped n m v -> ptyped n m (poly_pls u v).
Lemma insert_ptyped: forall n m z x u, mtyped n m x -> ptyped n m u -> ptyped n m (insert z x u).
Lemma mt_app: forall n m p h k, mtyped n m h -> mtyped m p k -> mtyped n p (h++k).
Lemma ldot_ptyped: forall n m p y q r, mtyped n m q -> ptyped m p r -> ptyped n p (ldot y q r).
Lemma rdot_ptyped: forall n m p y q r, mtyped m n q -> ptyped p m r -> ptyped p n (rdot y q r).
Lemma dot_ptyped: forall n m u, ptyped n m u -> forall p v, ptyped m p v -> ptyped n p (poly_dot u v).
Lemma eval_ptyped: forall n m u, typed n m u -> ptyped n m (eval u).
Theorem norm_typed: forall n m u, typed n m u -> typed n m (norm u).
lemmas about the copy function
Lemma copy_succ: forall x n m p, typed n m p -> equal n m (copy p (Psucc x)) (p + copy p x).
Lemma copy_compat: forall n m a b x, equal n m a b -> equal n m (copy a x) (copy b x).
Lemma copy_plus: forall x y n m p, typed n m p -> equal n m (copy p (x+y)) (copy p x + copy p y).
Lemma copy_pred: forall x n m p, typed n m p -> Plt 1 x -> equal n m (copy p (Ppred x)) (copy p x + - p).
Lemma copy_minus: forall x y n m p, typed n m p -> Plt y x -> equal n m (copy p (x-y)) (copy p x + - copy p y).
Lemma copy_dot: forall n m p a b x, typed n m a -> typed m p b -> equal n p (copy a x * b) (copy (a*b) x).
Lemma dot_copy: forall n m p a b x, typed m n a -> typed p m b -> equal p n (b * copy a x) (copy (b*a) x).
Lemma copy_mult: forall n m a x y, typed n m a -> equal n m (copy a (x*y)) (copy (copy a y) x).
Lemma readm_app: forall n m p a b, mtyped n m a -> mtyped m p b -> equal n p (readm (a++b)) (readm a * readm b).
Lemma copy_readm_app: forall n m p a b x y, mtyped n m a -> mtyped m p b ->
equal n p (copy (readm (a++b)) (x*y)) (copy (readm a) x * copy (readm b) y).
lemmas about readzm
Lemma zm_correct: forall n m z x p, mtyped n m x -> ptyped n m p ->
equal n m (zm z x p) (readzm (z,x) + p).
Lemma readzm_plus: forall x y n m p, mtyped n m p -> equal n m (readzm (x+y,p)%Z) (readzm (x,p) + readzm (y,p)).
Lemma readzm_zer: forall n m p, equal n m (readzm (0%Z,p)) 0.
Lemma readzm_neg: forall n m p x, mtyped n m p -> equal n m (readzm (Zopp x,p)) (-readzm (x,p)).
Lemma readzm_mult: forall n m p a b x y, mtyped n m a -> mtyped m p b ->
equal n p (readzm ((x * y)%Z, a++b)) (readzm (x, a) * readzm (y, b)).
correctness of poly_opp
correctness of poly_pls
Lemma pls_correct: forall n m u, ptyped n m u -> forall v, ptyped n m v ->
equal n m (poly_pls u v) (u+v).
correctness of insert
Lemma insert_correct: forall n m x u v, ptyped n m v -> mtyped n m u ->
equal n m (insert x u v) (read [(x,u)]+v).
lemmas about ldot and rdot
Lemma ldot_zer: forall n m p a b, ptyped m n b -> mtyped p m a -> equal p n (ldot 0 a b) 0.
Lemma ldot_neg: forall x n m p a b, ptyped m n b -> mtyped p m a -> equal p n (ldot (-x) a b) (-ldot x a b).
Lemma ldot_pos_correct: forall x n m p a b, ptyped m n b -> mtyped p m a ->
equal p n (ldot (Zpos x) a b) (copy (readm a) x * b).
Lemma rdot_zer: forall n m p a b, ptyped n m b -> mtyped m p a -> equal n p (rdot 0 a b) 0.
Lemma rdot_neg: forall x n m p a b, ptyped n m b -> mtyped m p a -> equal n p (rdot (-x) a b) (-rdot x a b).
Lemma rdot_pos_correct: forall x n m p a b, ptyped n m b -> mtyped m p a ->
equal n p (rdot (Zpos x) a b) (b * copy (readm a) x).
correctness of poly_dot
Lemma dot_correct: forall n m p u, ptyped n m u -> forall v, ptyped m p v ->
equal n p (poly_dot u v) (u*v).
summing up, we get the correctness of the norm function
Theorem norm_correct: forall n m u, typed n m u -> equal n m (norm u) u.
Lemma normalise: forall n m u v, typed n m u -> typed n m v -> equal n m (norm u) (norm v) -> equal n m u v.
End types.
trivial typing environment
== is the untyped equality
the following result is admitted since it is standard, a bit tedious, and does not involve types
Axiom eval_complete: forall u v, u == v -> eval u = eval v.
Theorem norm_complete: forall u v, u == v -> norm u = norm v.
Theorem norm_complete: forall u v, u == v -> norm u = norm v.
Section erase.
Variable I: Set.
Variables s t: X -> I.
Notation typed := (typed s t).
Notation equal := (equal s t).
untyping theorem for rings
Theorem untype: forall u v, u == v -> forall n m, typed n m u -> typed n m v -> equal n m u v.
End erase.
This page has been generated by coqdoc