coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] coq tatic help

From: Gaëtan Gilbert <gaetan.gilbert AT skyskimmer.net>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] coq tatic help
Date: Mon, 18 Mar 2019 14:42:34 +0100
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=gaetan.gilbert AT skyskimmer.net; spf=Pass smtp.mailfrom=gaetan.gilbert AT skyskimmer.net; spf=None smtp.helo=postmaster AT relay3-d.mail.gandi.net
Ironport-data: A9a23:mP2KEK2i0xSie0gXTfbDix16xS1kqk9dZch8hSBEBSB1pzcxvvu/+9 O5n/zm5GrHZeBxPX+umyhicVPPePsgR80UUcaZ5V7Xy/ZKpSYhxopsku5X75t1h6D5Mpdj83 I5P2LFc8A6vEl7OxPxteu0iZe9RMrsTHgRpNMJA9ESi3ejQ52DbnN08piputUG3G+mU56WpS sIkcXot5olqzv8BrA5Dt1jyfjo8HuPe7ExbPkwIexb837XwpRJ5qWnjgI3AaXFUQHRvSyHBg HDpLIXkS1JFnalLh2YQ48MWrrzKcHB6OZi+z0ap/Qe0eacesaUksZJOFg1nqcuFsV1rJVLz+ cdFb9ASA1yTBfD5bb9v07QVk48076fJ7svfufFp85AsvxnWWzDPfFXJOSwkLp+R9PS8t71s4 zs79dGekf5DuvOpW8EO/2i4NSj3kPuo2sIltU4y4iXGdu9AHphJFxOyHIzSZwc/CCPATo690 A/8dRLNBTu/08f4LrJO49zZsleLhfd3kggj5yPx6/qo28LVvRystNIC0ED+O0nIg/ftWX5Dj 4oukPwyQS34cadPTGdjp6Br9EZr5vdIBmBCGt2rawwVSXxR9TbiO7I07bLaQLwzDLXn71xYw +SP0tw1l4UPCgG4PO+lCujejK/UZk7R5vrgPEnK8M15ZZplwd/WsW4UKTvjhYks1uWByLpVx z7JmSFkOCwJi0c0/9W5SGIP6mDbD8Io1wWszYaQYy1JhWF9BxAMWZYy/lCx2e0LPjPr3SVZD xbidfAqyv1OpG7l8SvGslTMz2yUTvSKyK1cbA/zikllqaJo828eJanIXZXBhsjHJTioYoIEf 87uVIbKVsJ/NGnu5Ymd3Rd9Emq22GmqAO+wH7cIwENLBFeriEZEpd3ymVV6qPsGukjTPQzc3 KlzC+6ttB4cKzDw04Y+iTdY6w=
Ironport-phdr: 9a23:bmTeuhGJps7Foqre0/d+4p1GYnF86YWxBRYc798ds5kLTJ78oMSwAk XT6L1XgUPTWs2DsrQY0rKQ6/mocFdDyK7JiGoFfp1IWk1NouQttCtkPvS4D1bmJuXhdS0wEZ cKflZk+3amLRodQ56mNBXdrXKo8DEdBAj0OxZrKeTpAI7SiNm82/yv95HJbAhEmSaxbaluIB mrsA7cqtQYjYx+J6gr1xDHuGFIe+NYxWNpIVKcgRPx7dqu8ZBg7ipdpesv+9ZPXqvmcas4S6 dYDCk9PGAu+MLrrxjDQhCR6XYaT24bjwBHAwnB7BH9Q5fxri73vfdz1SWGIcH7S60/VDK/5K lpVRDokj8KOSMn/mHZisJ+j6xVrxyuqBN934Hab5qYNOZ9c67HYd8WWWRMU8RXWidcAo28dY wPD+8ZMOhZtYb6u0cOogG4BQa0Be3vyztIiWTo0q0gz+QqDAbL3AM6EN0QrHTbttP1OL0dUe C0yKnH1ivMb+lK2Trm84jIcRAgoeqPXbJxdMrRzFcgFxnfglWWt4PlIyqY2+IQuGaY9+ptTf yjh3Mlpg1roDWj2t0ghpTKi48b0FzI6CF0zYYtKdGlTEN2b8SoHZtfui2ANYZ7Q9kuTmFmtS s817YIo4S0fDIQx5Qi3xPfa+KIc4yP4h/7TuaePzN4i2hleb+xnhq97FKsyujmWcm11FZGtC VFncPKtn8Q1hzf8M6HReVh/ku52DaP0R7c6v1cLEwqiKbWKYQtz7wsmpYJrEjOHSH7lF/rgK KSdkgo4u2o5P7mYrXiqJ+cLYh0igTmP6QhgMOwH/g4PRIIX2SB9uS81bnj8lbnT7VQkv07ib LZsJPaJMQApa65AgpV0oM95BalFTum1soXnWUfIFJfZB2Hl5TpO03JIP3gEfi/hE2snC53yP DCI73uGY7ALmPDkbfkZbZy8VRQyAs1zdBF5pJbEKsNIPzpWhy5iNuNBRggdgew3uzPCdNn14 pYV3jcLLWeNfb9uNyU7+QYDOiIboIPpH6pJPEo+/foy3A4nVUQZ7WBxpgGc3O5G/FrOQOfbG a60YRJKnsDogdrFL+is1aFSzMGPy/uDZJ53SkyDcedNamGXpqk2eLTxySqBZ5XY2VLEBaKHG u6L9zZCcdJUzqbJ4paqhJBVbWlTNV8hwujsAbrkP9raO/d+yleupvl2Nkz4eDPx0lrpG5ESv +F2mTIdFla22YBRjs4xqd6+BIv0VSSyqt5hvlVD5pV6u8bCwo=

Try "unfold ea_in_range in H"

Gaëtan Gilbert

On 18/03/2019 14:40, 朱立平 wrote:

Thanks Maximilian.
But after apply tatics:
/intros./
/unfold ea_in_range./
It seems unfold does nothing.

1 subgoals
a : nat
H : ea_in_range a
______________________________________(1/1)
a + 3 < 6

Can you proove the goal for me?

At 2019-03-17 20:01:19, "Maximilian Wuttke"
<s8mawutt AT stud.uni-saarland.de>
wrote:

`omega` doesn't unfold definitions.
You need to unfold `ea_in_range` first.

```
Lemma test2:
forall a, ea_in_range a -> a+3<6.
Proof.
unfold ea_in_range.
intros.
omega.
Qed.
```

On 17/03/2019 12:27, 朱立平 wrote:

Since omega works in the following proof.
Require Import ZArith.

/Lemma test1:/
/ forall a, a<3 -> a+3<6./
/Proof./
/intros./
/omega./
/Qed./

I wonder why error occurs at this:
/Definition ea_in_range (ea:nat) : Prop := ea < 3./

/Lemma test2:/
/ forall a, ea_in_range a -> a+3<6./
/Proof./
/intros./
/omega. /
Error: Omega can't solve this system

Best Regards,
Julian

[Coq-Club] coq tatic help, 朱立平, 03/17/2019
- Re: [Coq-Club] coq tatic help, Maximilian Wuttke, 03/17/2019
  - Re:[Coq-Club] coq tatic help, 朱立平, 03/18/2019
    - Re: [Coq-Club] coq tatic help, Gaëtan Gilbert, 03/18/2019
      - Re: [Coq-Club] coq tatic help, Zhu, 03/20/2019
    - Re: [Coq-Club] coq tatic help, mukesh tiwari, 03/18/2019