diff options
author | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-08-05 19:04:16 +0000 |
---|---|---|
committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-08-05 19:04:16 +0000 |
commit | 83c56744d7e232abeb5f23e6d0f23cd0abc14a9c (patch) | |
tree | 6d7d4c2ce3bb159b8f81a4193abde1e3573c28d4 /theories/Arith/Between.v | |
parent | f7351ff222bad0cc906dbee3c06b20babf920100 (diff) |
Expérimentation de NewDestruct et parfois NewInduction
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1880 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Arith/Between.v')
-rwxr-xr-x | theories/Arith/Between.v | 58 |
1 files changed, 29 insertions, 29 deletions
diff --git a/theories/Arith/Between.v b/theories/Arith/Between.v index ab22eca22..e6b444601 100755 --- a/theories/Arith/Between.v +++ b/theories/Arith/Between.v @@ -22,29 +22,29 @@ Hint constr_between : arith v62 := Constructors between. Lemma bet_eq : (k,l:nat)(l=k)->(between k l). Proof. -Induction 1; Auto with arith. +NewInduction 1; Auto with arith. Qed. Hints Resolve bet_eq : arith v62. Lemma between_le : (k,l:nat)(between k l)->(le k l). Proof. -Induction 1; Auto with arith. +NewInduction 1; Auto with arith. Qed. Hints Immediate between_le : arith v62. Lemma between_Sk_l : (k,l:nat)(between k l)->(le (S k) l)->(between (S k) l). Proof. -Induction 1. +NewInduction 1. Intros; Absurd (le (S k) k); Auto with arith. -Induction 1; Auto with arith. +Induction H; Auto with arith. Qed. Hints Resolve between_Sk_l : arith v62. Lemma between_restr : (k,l,m:nat)(le k l)->(le l m)->(between k m)->(between l m). Proof. -Induction 1; Auto with arith. +NewInduction 1; Auto with arith. Qed. Inductive exists [k:nat] : nat -> Prop @@ -55,7 +55,7 @@ Hint constr_exists : arith v62 := Constructors exists. Lemma exists_le_S : (k,l:nat)(exists k l)->(le (S k) l). Proof. -Induction 1; Auto with arith. +NewInduction 1; Auto with arith. Qed. Lemma exists_lt : (k,l:nat)(exists k l)->(lt k l). @@ -78,55 +78,55 @@ Hints Resolve in_int_intro : arith v62. Lemma in_int_lt : (p,q,r:nat)(in_int p q r)->(lt p q). Proof. -Induction 1; Intros. +NewInduction 1; Intros. Apply le_lt_trans with r; Auto with arith. Qed. Lemma in_int_p_Sq : (p,q,r:nat)(in_int p (S q) r)->((in_int p q r) \/ <nat>r=q). Proof. -Induction 1; Intros. +NewInduction 1; Intros. Elim (le_lt_or_eq r q); Auto with arith. Qed. Lemma in_int_S : (p,q,r:nat)(in_int p q r)->(in_int p (S q) r). Proof. -Induction 1;Auto with arith. +NewInduction 1;Auto with arith. Qed. Hints Resolve in_int_S : arith v62. Lemma in_int_Sp_q : (p,q,r:nat)(in_int (S p) q r)->(in_int p q r). Proof. -Induction 1; Auto with arith. +NewInduction 1; Auto with arith. Qed. Hints Immediate in_int_Sp_q : arith v62. Lemma between_in_int : (k,l:nat)(between k l)->(r:nat)(in_int k l r)->(P r). Proof. -Induction 1; Intros. +NewInduction 1; Intros. Absurd (lt k k); Auto with arith. Apply in_int_lt with r; Auto with arith. -Elim (in_int_p_Sq k l0 r); Intros; Auto with arith. -Rewrite H4; Trivial with arith. +Elim (in_int_p_Sq k l r); Intros; Auto with arith. +Rewrite H2; Trivial with arith. Qed. Lemma in_int_between : (k,l:nat)(le k l)->((r:nat)(in_int k l r)->(P r))->(between k l). Proof. -Induction 1; Auto with arith. +NewInduction 1; Auto with arith. Qed. Lemma exists_in_int : (k,l:nat)(exists k l)->(EX m:nat | (in_int k l m) & (Q m)). Proof. -Induction 1. -Induction 2; Intros p inp Qp; Exists p; Auto with arith. -Intros; Exists l0; Auto with arith. +NewInduction 1. +Case IHexists; Intros p inp Qp; Exists p; Auto with arith. +Exists l; Auto with arith. Qed. Lemma in_int_exists : (k,l,r:nat)(in_int k l r)->(Q r)->(exists k l). Proof. -Induction 1; Intros. +NewInduction 1; Intros. Elim H1; Auto with arith. Qed. @@ -134,23 +134,23 @@ Lemma between_or_exists : (k,l:nat)(le k l)->((n:nat)(in_int k l n)->((P n)\/(Q n))) ->((between k l)\/(exists k l)). Proof. -Induction 1; Intros; Auto with arith. -Elim H1; Intro; Auto with arith. -Elim (H2 m); Auto with arith. +NewInduction 1; Intros; Auto with arith. +Elim IHle; Intro; Auto with arith. +Elim (H0 m); Auto with arith. Qed. Lemma between_not_exists : (k,l:nat)(between k l)-> ((n:nat)(in_int k l n) -> (P n) -> ~(Q n)) -> ~(exists k l). Proof. -Induction 1; Red; Intros. +NewInduction 1; Red; Intros. Absurd (lt k k); Auto with arith. -Absurd (Q l0); Auto with arith. -Elim (exists_in_int k (S l0)); Auto with arith; Intros l' inl' Ql'. -Replace l0 with l'; Auto with arith. +Absurd (Q l); Auto with arith. +Elim (exists_in_int k (S l)); Auto with arith; Intros l' inl' Ql'. +Replace l with l'; Auto with arith. Elim inl'; Intros. -Elim (le_lt_or_eq l' l0); Auto with arith; Intros. -Absurd (exists k l0); Auto with arith. +Elim (le_lt_or_eq l' l); Auto with arith; Intros. +Absurd (exists k l); Auto with arith. Apply in_int_exists with l'; Auto with arith. Qed. @@ -161,7 +161,7 @@ Inductive nth [init:nat] : nat->nat->Prop Lemma nth_le : (init,l,n:nat)(nth init l n)->(le init l). Proof. -Induction 1; Intros; Auto with arith. +NewInduction 1; Intros; Auto with arith. Apply le_trans with (S k); Auto with arith. Qed. @@ -169,7 +169,7 @@ Definition eventually := [n:nat](EX k:nat | (le k n) & (Q k)). Lemma event_O : (eventually O)->(Q O). Proof. -Induction 1; Intros. +NewInduction 1; Intros. Replace O with x; Auto with arith. Qed. |