diff options
| author | herbelin | 2004-03-11 22:33:52 +0000 |
|---|---|---|
| committer | herbelin | 2004-03-11 22:33:52 +0000 |
| commit | c981c0974e76eab39d916f79374b6432cf188558 (patch) | |
| tree | 5ee6352eba2e14ff790bd82f142ef1baee3df23d | |
| parent | 1c397c94838bb560d4a1e93a5cf22f79bae28be6 (diff) | |
Ajout d'un vieil exemple de N. Magaud
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5457 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | test-suite/success/eauto.v | 13 |
1 files changed, 12 insertions, 1 deletions
diff --git a/test-suite/success/eauto.v b/test-suite/success/eauto.v index 8a5e146d4e..999cb1212a 100644 --- a/test-suite/success/eauto.v +++ b/test-suite/success/eauto.v @@ -33,6 +33,17 @@ Intros. EAuto with essai. Save. +(* Example from Nicolas Magaud on coq-club - Jul 2000 *) +Definition Nat: Set := nat. +Parameter S':Nat ->Nat. +Parameter plus':Nat -> Nat ->Nat. - +Lemma simpl_plus_l_rr1: + ((n0:Nat) ((m, p:Nat) (plus' n0 m)=(plus' n0 p) ->m=p) -> + (m, p:Nat) (S' (plus' n0 m))=(S' (plus' n0 p)) ->m=p) -> + (n:Nat) ((m, p:Nat) (plus' n m)=(plus' n p) ->m=p) -> + (m, p:Nat) (S' (plus' n m))=(S' (plus' n p)) ->m=p. +Intros. +EAuto. (* does EApply H *) +Qed. |