Permalink
Browse files

Added properties of multiplication to nat.tt

(Commutativity, distributivity and associativity)

darcs-hash:20060906143920-974a0-8feb5810a6fe45455631b2c58ceda60f697cc127.gz
  • Loading branch information...
eb
eb committed Sep 6, 2006
1 parent 3628672 commit c9c1401e82d851a4412d01702299004d46a799ab
Showing with 96 additions and 6 deletions.
  1. +1 −1 Ivor/Tactics.lhs
  2. +1 −1 Makefile
  3. +45 −0 examplett/nat.tt
  4. +49 −4 tests/nat.tt
View
@@ -85,7 +85,7 @@ no guesses attached (False).
> fh env (Stage (Escape t)) = fh env t
> fh _ _ = []
>
-> fhb env (Let x) = fh env x
+> -- fhb env (Let x) = fh env x
> fhb env (Guess x) = fh env x
> fhb env _ = []
View
@@ -1,7 +1,7 @@
DB = --user
PREFIX = $(HOME)
# Set this to -p for profiling libraries too
-PROFILE = -p
+PROFILE =
GHCOPTS =
package:
View
@@ -180,3 +180,48 @@ refine refl;
Qed;
Freeze multnSm;
+mult_comm : (m,n:Nat) -> (Eq _ (mult m n) (mult n m));
+intro m;
+induction m;
+intros;
+replace (multnO n);
+refine refl;
+intros;
+replace (multnSm n0 k);
+replace sym (k_IH n0);
+refine refl;
+Qed;
+Freeze mult_comm;
+
+mult_distrib:(m,n,p:Nat)(Eq _ (plus (mult m p) (mult n p))
+ (mult (plus m n) p));
+intros;
+induction m;
+refine refl;
+intros;
+equiv Eq _ (plus (plus p (mult k p)) (mult n p))
+ (plus p (mult (plus k n) p));
+replace sym k_IH;
+generalise mult k p;
+generalise mult n p;
+intro x y;
+replace plus_assoc p y x;
+refine refl;
+Qed;
+
+mult_assoc:(m,n,p:Nat)(Eq _ (mult m (mult n p)) (mult (mult m n) p));
+intro m;
+induction m;
+intros;
+compute;
+refine refl;
+intros;
+equiv Eq _ (plus (mult n0 p0) (mult k (mult n0 p0)))
+ (mult (plus n0 (mult k n0)) p0);
+replace k_IH n0 p0;
+generalise mult k n0;
+intros;
+replace mult_distrib n0 x p0;
+refine refl;
+Qed;
+
View
@@ -3,16 +3,16 @@ Load "logic.tt";
Data Nat:* = O:Nat | S:(k:Nat)Nat;
-plus : (m:Nat)(n:Nat)Nat;
+plus : Nat -> Nat -> Nat;
intro m;
induction m;
intros;
-fill n;
+fill X0;
intros;
-fill S (k_IH n0);
+fill S (k_IH X1);
Qed;
-mult : (m:Nat)(n:Nat)Nat;
+mult : (m:Nat) -> (n:Nat) -> Nat;
intro m;
induction m;
intros;
@@ -180,3 +180,48 @@ refine refl;
Qed;
Freeze multnSm;
+mult_comm : (m,n:Nat) -> (Eq _ (mult m n) (mult n m));
+intro m;
+induction m;
+intros;
+replace (multnO n);
+refine refl;
+intros;
+replace (multnSm n0 k);
+replace sym (k_IH n0);
+refine refl;
+Qed;
+Freeze mult_comm;
+
+mult_distrib:(m,n,p:Nat)(Eq _ (plus (mult m p) (mult n p))
+ (mult (plus m n) p));
+intros;
+induction m;
+refine refl;
+intros;
+equiv Eq _ (plus (plus p (mult k p)) (mult n p))
+ (plus p (mult (plus k n) p));
+replace sym k_IH;
+generalise mult k p;
+generalise mult n p;
+intro x y;
+replace plus_assoc p y x;
+refine refl;
+Qed;
+
+mult_assoc:(m,n,p:Nat)(Eq _ (mult m (mult n p)) (mult (mult m n) p));
+intro m;
+induction m;
+intros;
+compute;
+refine refl;
+intros;
+equiv Eq _ (plus (mult n0 p0) (mult k (mult n0 p0)))
+ (mult (plus n0 (mult k n0)) p0);
+replace k_IH n0 p0;
+generalise mult k n0;
+intros;
+replace mult_distrib n0 x p0;
+refine refl;
+Qed;
+

0 comments on commit c9c1401

Please sign in to comment.