coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] How much can I expect from higher-order unification?

From: Enrico Tassi <enrico.tassi AT inria.fr>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] How much can I expect from higher-order unification?
Date: Fri, 18 May 2018 21:57:48 +0200
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=enrico.tassi AT inria.fr; spf=None smtp.mailfrom=gares AT fettunta.org; spf=None smtp.helo=postmaster AT fettunta.org
Ironport-phdr: 9a23:Uyo99RUtg6AJVgObrjVL2NMqlR7V8LGtZVwlr6E/grcLSJyIuqrYYxeFt8tkgFKBZ4jH8fUM07OQ7/i7HzRYqb+681k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i764jEdAAjwOhRoLerpBIHSk9631+ev8JHPfglEnjWwba98IRmssQndqtQdjJd/JKo21hbHuGZDdf5MxWNvK1KTnhL86dm18ZV+7SleuO8v+tBZX6nicKs2UbJXDDI9M2Ao/8LrrgXMTRGO5nQHTGoblAdDDhXf4xH7WpfxtTb6tvZ41SKHM8D6Uaw4VDK/5KptVRTmijoINyQh/W/ZisJ+kr9VrhGvpxNw34HbfYOaO/Rlc6PBYd8XX3ZNUtpLWiBfBI63cosBD/AGPeZdt4TzqF0OrQG/BQawA+Pk1yFGiWXt3a0h0uQqDAbL0xImH9IUsXTbsNL1OL0OUe+v16nI1jTDYuhX2Tf78ojIcwoureuCXbJqaMfcz1QkGQ3CjlWVs4PlPjWV2/wMs2id9epgVPigh3QpqwFrpDWk28QiipHRi48RxV3I7zt1zYgvKdC5TEN3e8OoHIVSui2CNIZ7QdkuT3xqtSs50LELvZG2cDIXxJg72hLSbeGMfZKS7RL5TumRJC91hHJ7d7K7gBa/6UagxfPgVsmozVZKqDZFncPWunAKzRzT5dCLSvp7/ki/xTaCzwTe5+5eLUwqm6fXMZ8sz7oqmpYOr0jOHDf6mEDsg6+XckUk9PKo6+PiYrj+qZ+TLZV0hR/lMqk1lMywH/g4MhQTX2id5eSzzqfv/UrjQLVFlvE2iLXWsIjGJcQHoa60GxNa0oE66xqmEzim1MkYkmIcIVJeeBOHipDpNEvULPD5C/e/mVWsny1xy/DIJL2ySqnKe3PEifLqeat3w09a0gs6i95FtLxODbRUDfTpW0T2/ODRFQQ4e1i5xfzmA9I7yooFQmOnA6mDMaqUv0XetbFnGPWFeIJA4GW1EPMi/fO71SZoy29YRrGg2N4sUF79G/1nJ0uDZn+13oUPHHsWowwiRartklLQCWcPNUb3ZLo143QAMKzjFZ3KH9j/gbqb3S79EIcEPjkbWGDJKm/hcsC/Y9lJaC+WJZY9wDIJSaS8TZMokxa0u12ixg==

On Thu, May 17, 2018 at 08:18:05PM -0400, Joachim Breitner wrote:
> Unable to unify "?P (take n b) n b" with
> "length (take n b) = Init.Nat.min n (length b)".

The elim tactic of the SSReflect proof language is likely to able to
synthesize P for you: it does not use HO unification but rather guess P
by abstracting the goal over all the arguments P gets in the conclusion
of the lemma, here (take n b).

See:

https://coq.inria.fr/distrib/current/refman/proof-engine/ssreflect-proof-language.html#interpreting-eliminations

The example about plus_ind is quite close to yours.

Best,
--
Enrico Tassi

[Coq-Club] How much can I expect from higher-order unification?, Joachim Breitner, 05/18/2018
- Re: [Coq-Club] How much can I expect from higher-order unification?, Pierre Courtieu, 05/18/2018
- Re: [Coq-Club] How much can I expect from higher-order unification?, Enrico Tassi, 05/18/2018