Load "eq.tt"; Load "logic.tt"; Data Nat:* = O:Nat | S:(k:Nat)Nat; Match plus : Nat->Nat->Nat = plus O y = y | plus (S k) y = S (plus k y); Match mult : Nat->Nat->Nat = mult O y = O | mult (S k) y = plus y (mult k y); simplifyO:(n:_)(Eq _ _ (plus O n) n); intros; refine refl; Qed; simplifyS:(m,n:_)(Eq _ _ (plus (S m) n) (S (plus m n))); intros; refine refl; Qed; eq_resp_S:(n,m:_)(q:Eq _ _ n m)(Eq _ _ (S n) (S m)); intros; fill (eq_resp_f _ _ S n m q); Qed; Freeze eq_resp_S; s_injective:(n,m:_)(q:Eq _ _ (S n) (S m))(Eq _ _ n m); intros; local unS:(m:Nat)Nat; intros; induction m0; fill n; intros; fill k; fill eq_resp_f _ _ unS _ _ q; Qed; Freeze s_injective; notO_S:(k:_)(not (Eq _ _ O (S k))); intros; compute; intro q; local dmotive : (x:Nat)(q:Eq _ _ O x)*; intros; induction x; fill True; intros; fill False; fill EqElim _ _ _ q dmotive II; Qed; Freeze notO_S; notn_S:(n:_)(not (Eq _ _ n (S n))); intro; induction n; fill notO_S O; intros; unfold not; intros; claim q:Eq _ _ k (S k); fill k_IH q; refine s_injective; fill a; Qed; Freeze notn_S; discriminate_Nat:(A,k:_)(q:Eq _ _ O (S k))A; intros; local false:False; fill notO_S k q; induction false; Qed; Freeze discriminate_Nat; plusnO:(n:_)(Eq _ _ (plus n O) n); intro; induction n; refine refl; intros; equiv Eq _ _ (S (plus k O)) (S k); refine eq_resp_S; fill k_IH; Qed; Freeze plusnO; plusnSm:(n,m:_)(Eq _ _ (plus n (S m)) (S (plus n m))); intros; induction n; refine refl; intros; refine eq_resp_S; fill k_IH; Qed; Freeze plusnSm; plus_comm:(n,m:_)(Eq _ _ (plus n m) (plus m n)); intros; induction n; refine sym; refine plusnO; intros; equiv Eq _ _ (S (plus k m)) (plus m (S k)); replace k_IH; refine sym; refine plusnSm; Qed; Freeze plus_comm; plus_assoc:(m,n,p:_)(Eq _ _ (plus m (plus n p)) (plus (plus m n) p)); intros; induction m; refine refl; intros; equiv Eq _ _ (S (plus k (plus n p))) (plus (S (plus k n)) p); replace k_IH; refine refl; Qed; Freeze plus_assoc; plus_eq_fst : (m,n,p:_)(q:Eq _ _ (plus p m) (plus p n))(Eq _ _ m n); intro m n p; induction p; intros; fill q; intros; refine k_IH; refine s_injective; refine q0; Qed; Freeze plus_eq_fst; plus_eq_fst_sym : (m,n,p:_)(q:Eq _ _ (plus m p) (plus n p))(Eq _ _ m n); intro m n p; replace plus_comm m p; replace plus_comm n p; intros; fill plus_eq_fst m n p q; Qed; Freeze plus_eq_fst_sym; multnO:(n:_)(Eq _ _ (mult n O) O); intro; induction n; refine refl; intros; equiv Eq _ _ (plus O (mult k O)) O; replace k_IH; refine refl; Qed; Freeze multnO; multnSm:(n,m:_)(Eq _ _ (mult n (S m)) (plus n (mult n m))); intro; induction n; intros; refine refl; intros; equiv Eq _ _ (S (plus m0 (mult k (S m0)))) (S (plus k (plus m0 (mult k m0)))); refine eq_resp_S; replace (k_IH m0); generalise mult k m0; intros; replace (plus_comm m0 x); replace (plus_assoc k x m0); replace (plus_comm m0 (plus k x)); refine refl; Qed; Freeze multnSm;