From 292798b0303eb7f580d73b68fce708289645d97d Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 1 Jun 2005 11:06:46 +0000 Subject: [PATCH] fix --- helm/matita/tests/match.ma | 74 +++++++++++++++++++------------------- 1 file changed, 37 insertions(+), 37 deletions(-) diff --git a/helm/matita/tests/match.ma b/helm/matita/tests/match.ma index f9b8a0fb6..732e96fa0 100644 --- a/helm/matita/tests/match.ma +++ b/helm/matita/tests/match.ma @@ -7,18 +7,18 @@ definition Not: Prop \to Prop \def \lambda A:Prop. (A \to False). theorem absurd : \forall A,C:Prop. A \to Not A \to C. -intro.cut False.elim Hcut.apply H1.assumption. +intros.cut False.elim Hcut.apply H1.assumption. qed. inductive And (A,B:Prop) : Prop \def conj : A \to B \to (And A B). theorem proj1: \forall A,B:Prop. (And A B) \to A. -intro. elim H. assumption. +intros. elim H. assumption. qed. theorem proj2: \forall A,B:Prop. (And A B) \to A. -intro. elim H. assumption. +intros. elim H. assumption. qed. inductive Or (A,B:Prop) : Prop \def @@ -35,23 +35,23 @@ inductive eq (A:Type) (x:A) : A \to Prop \def refl_equal : eq A x x. theorem sym_eq : \forall A:Type.\forall x,y:A. eq A x y \to eq A y x. -intro. elim H. apply refl_equal. +intros. elim H. apply refl_equal. qed. theorem trans_eq : \forall A:Type. \forall x,y,z:A. eq A x y \to eq A y z \to eq A x z. -intro.elim H1.assumption. +intros.elim H1.assumption. qed. theorem f_equal: \forall A,B:Type.\forall f:A\to B. \forall x,y:A. eq A x y \to eq B (f x) (f y). -intro.elim H.apply refl_equal. +intros.elim H.apply refl_equal. qed. theorem f_equal2: \forall A,B,C:Type.\forall f:A\to B \to C. \forall x1,x2:A. \forall y1,y2:B. eq A x1 x2\to eq B y1 y2\to eq C (f x1 y1) (f x2 y2). -intro.elim H1.elim H.apply refl_equal. +intros.elim H1.elim H.apply refl_equal. qed. inductive nat : Set \def @@ -65,18 +65,18 @@ definition pred: nat \to nat \def theorem pred_Sn : \forall n:nat. (eq nat n (pred (S n))). -intro.apply refl_equal. +intros.apply refl_equal. qed. theorem injective_S : \forall n,m:nat. (eq nat (S n) (S m)) \to (eq nat n m). -intro.(elim (sym_eq ? ? ? (pred_Sn n))).(elim (sym_eq ? ? ? (pred_Sn m))). +intros.(elim (sym_eq ? ? ? (pred_Sn n))).(elim (sym_eq ? ? ? (pred_Sn m))). apply f_equal. assumption. qed. theorem not_eq_S : \forall n,m:nat. Not (eq nat n m) \to Not (eq nat (S n) (S m)). -intro. simplify.intro. +intros. simplify.intros. apply H.apply injective_S.assumption. qed. @@ -87,13 +87,13 @@ definition not_zero : nat \to Prop \def | (S p) \Rightarrow True ]. theorem O_S : \forall n:nat. Not (eq nat O (S n)). -intro.simplify.intro. +intros.simplify.intros. cut (not_zero O).exact Hcut.elim (sym_eq ? ? ? H). exact I. qed. theorem n_Sn : \forall n:nat. Not (eq nat n (S n)). -intro.elim n.apply O_S.apply not_eq_S.assumption. +intros.elim n.apply O_S.apply not_eq_S.assumption. qed. @@ -106,21 +106,21 @@ in plus. theorem plus_n_O: \forall n:nat. eq nat n (plus n O). -intro.elim n.simplify.apply refl_equal.simplify.apply f_equal.assumption. +intros.elim n.simplify.apply refl_equal.simplify.apply f_equal.assumption. qed. theorem plus_n_Sm : \forall n,m:nat. eq nat (S (plus n m)) (plus n (S m)). -intro.elim n.simplify.apply refl_equal.simplify.apply f_equal.assumption. +intros.elim n.simplify.apply refl_equal.simplify.apply f_equal.assumption. qed. theorem sym_plus: \forall n,m:nat. eq nat (plus n m) (plus m n). -intro.elim n.simplify.apply plus_n_O. +intros.elim n.simplify.apply plus_n_O. simplify.elim (sym_eq ? ? ? H).apply plus_n_Sm. qed. theorem assoc_plus: \forall n,m,p:nat. eq nat (plus (plus n m) p) (plus n (plus m p)). -intro.elim n.simplify.apply refl_equal.simplify.apply f_equal.assumption. +intros.elim n.simplify.apply refl_equal.simplify.apply f_equal.assumption. qed. definition times : nat \to nat \to nat \def @@ -132,12 +132,12 @@ in times. theorem times_n_O: \forall n:nat. eq nat O (times n O). -intro.elim n.simplify.apply refl_equal.simplify.assumption. +intros.elim n.simplify.apply refl_equal.simplify.assumption. qed. theorem times_n_Sm : \forall n,m:nat. eq nat (plus n (times n m)) (times n (S m)). -intro.elim n.simplify.apply refl_equal. +intros.elim n.simplify.apply refl_equal. simplify.apply f_equal.elim H. apply trans_eq ? ? (plus (plus e m) (times e m)).apply sym_eq. apply assoc_plus.apply trans_eq ? ? (plus (plus m e) (times e m)). @@ -147,7 +147,7 @@ qed. theorem sym_times : \forall n,m:nat. eq nat (times n m) (times m n). -intro.elim n.simplify.apply times_n_O. +intros.elim n.simplify.apply times_n_O. simplify.elim (sym_eq ? ? ? H).apply times_n_Sm. qed. @@ -165,7 +165,7 @@ minus. theorem nat_case : \forall n:nat.\forall P:nat \to Prop. P O \to (\forall m:nat. P (S m)) \to P n. -intro.elim n.assumption.apply H1. +intros.elim n.assumption.apply H1. qed. theorem nat_double_ind : @@ -173,8 +173,8 @@ theorem nat_double_ind : (\forall n:nat. R O n) \to (\forall n:nat. R (S n) O) \to (\forall n,m:nat. R n m \to R (S n) (S m)) \to \forall n,m:nat. R n m. -intro.cut \forall m:nat.R n m.apply Hcut.elim n.apply H. -apply nat_case m1.apply H1.intro.apply H2. apply H3. +intros.cut \forall m:nat.R n m.apply Hcut.elim n.apply H. +apply nat_case m1.apply H1.intros.apply H2. apply H3. qed. inductive bool : Set \def @@ -212,60 +212,60 @@ inductive le (n:nat) : nat \to Prop \def | le_S : \forall m:nat. le n m \to le n (S m). theorem trans_le: \forall n,m,p:nat. le n m \to le m p \to le n p. -intro. +intros. elim H1.assumption. apply le_S.assumption. qed. theorem le_n_S: \forall n,m:nat. le n m \to le (S n) (S m). -intro.elim H. +intros.elim H. apply le_n.apply le_S.assumption. qed. theorem le_O_n : \forall n:nat. le O n. -intro.elim n.apply le_n.apply le_S. assumption. +intros.elim n.apply le_n.apply le_S. assumption. qed. theorem le_n_Sn : \forall n:nat. le n (S n). -intro. apply le_S.apply le_n. +intros. apply le_S.apply le_n. qed. theorem le_pred_n : \forall n:nat. le (pred n) n. -intro.elim n.simplify.apply le_n.simplify. +intros.elim n.simplify.apply le_n.simplify. apply le_n_Sn. qed. theorem not_zero_le : \forall n,m:nat. (le (S n) m ) \to not_zero m. -intro.elim H.exact I.exact I. +intros.elim H.exact I.exact I. qed. theorem le_Sn_O: \forall n:nat. Not (le (S n) O). -intro.simplify.intro.apply not_zero_le ? O H. +intros.simplify.intros.apply not_zero_le ? O H. qed. theorem le_n_O_eq : \forall n:nat. (le n O) \to (eq nat O n). -intro.cut (le n O) \to (eq nat O n).apply Hcut. assumption. +intros.cut (le n O) \to (eq nat O n).apply Hcut. assumption. elim n.apply refl_equal.apply False_ind.apply (le_Sn_O ? H2). qed. theorem le_S_n : \forall n,m:nat. le (S n) (S m) \to le n m. -intro.cut le (pred (S n)) (pred (S m)).exact Hcut. +intros.cut le (pred (S n)) (pred (S m)).exact Hcut. elim H.apply le_n.apply trans_le ? (pred x).assumption. apply le_pred_n. qed. theorem le_Sn_n : \forall n:nat. Not (le (S n) n). -intro.elim n.apply le_Sn_O.simplify.intro. +intros.elim n.apply le_Sn_O.simplify.intros. cut le (S e) e.apply H.assumption.apply le_S_n.assumption. qed. theorem le_antisym : \forall n,m:nat. (le n m) \to (le m n) \to (eq nat n m). -intro.cut (le n m) \to (le m n) \to (eq nat n m).exact Hcut H H1. +intros.cut (le n m) \to (le m n) \to (eq nat n m).exact Hcut H H1. apply nat_double_ind (\lambda n,m.((le n m) \to (le m n) \to eq nat n m)). -intro.whd.intro. +intros.whd.intros. apply le_n_O_eq.assumption. -intro.whd.intro.apply sym_eq.apply le_n_O_eq.assumption. -intro.whd.intro.apply f_equal.apply H2. +intros.whd.intros.apply sym_eq.apply le_n_O_eq.assumption. +intros.whd.intros.apply f_equal.apply H2. apply le_S_n.assumption. apply le_S_n.assumption. qed. @@ -288,5 +288,5 @@ simplify.intros.apply le_O_n. simplify.exact le_Sn_O. intros 2.simplify.elim (leb n1 m1). simplify.apply le_n_S.apply H. -simplify.intro.apply H.apply le_S_n.assumption. +simplify.intros.apply H.apply le_S_n.assumption. qed. -- 2.39.2