Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Getting "computing" proof terms with dependent types / reduction of matches with single pattern

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Getting "computing" proof terms with dependent types / reduction of matches with single pattern


Chronological Thread 
  • From: Jonathan Leivent <jonikelee AT gmail.com>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] Getting "computing" proof terms with dependent types / reduction of matches with single pattern
  • Date: Tue, 6 Sep 2016 12:29:16 -0400
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=jonikelee AT gmail.com; spf=Pass smtp.mailfrom=jonikelee AT gmail.com; spf=None smtp.helo=postmaster AT mail-qt0-f176.google.com
  • Ironport-phdr: 9a23:RWqWnxyTSZVQal3XCy+O+j09IxM/srCxBDY+r6Qd0u0SIJqq85mqBkHD//Il1AaPBtSCra8VwLqH++C4ACpbvsbH6ChDOLV3FDY7yuwu1zQ6B8CEDUCpZNXLVAcdWPp4aVl+4nugOlJUEsutL3fbo3m18CJAUk6nbVk9dazJHdvZiN3y3OSv8bXSZR9JjXyze+BcNhKz+CfWsMAKgYJkYoI8ywXEpGcAL+ZRw2JrKFaekj7z486x+Nho9CEG6KFpzNJJTaivJ/dwdrdfFjlza20=


On 09/06/2016 12:12 PM, Matthieu Sozeau wrote:
...
In effect, this would be what the definitional version of uniqueness of
identity proofs (aka the K rule/axiom) would give you, i.e. it would use
type information to convert plus_n_Sm 0 1 : S (0 + 1) = 0 + S 1 to eq_refl
: 2 = 2. This rule is not part of Coq's type theory (and neither from
standard Martin-Löf Type Theory).

But, you can use Eqdep_dec.UIP_refl_nat to rewrite those match discriminees down to eq_refl.

-- Jonathan


Archive powered by MHonArc 2.6.18.

Top of Page