coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Not enough information to resolve this refine goal

From: Maximilian Wuttke <mwuttke97 AT posteo.de>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Not enough information to resolve this refine goal
Date: Thu, 1 Oct 2020 03:12:59 +0200
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=mwuttke97 AT posteo.de; spf=Pass smtp.mailfrom=mwuttke97 AT posteo.de; spf=None smtp.helo=postmaster AT mout01.posteo.de
Ironport-phdr: 9a23:X/U3qRXXOzKakfT1ZMkca1MlNMDV8LGtZVwlr6E/grcLSJyIuqrYbBWBt8tkgFKBZ4jH8fUM07OQ7/m/Hzdbqsrd+Fk5M7V0HycfjssXmwFySOWkMmbcaMDQUiohAc5ZX0Vk9XzoeWJcGcL5ekGA6ibqtW1aFRrwLxd6KfroEYDOkcu3y/qy+5rOaAlUmTaxe7x/IAi0oAnLuMQbj4RuJ6k+xxDUvnZGZuNayH9yK1mOhRj8/MCw/JBi8yRUpf0s8tNLXLv5caolU7FWFSwqPG8p6sLlsxnDVhaP6WAHUmoKiBpIAhPK4w/8U5zsryb1rOt92C2dPc3rUbA5XCmp4ql3RBP0jioMKjg0+3zVhMNtlqJWuAyvpxJ/zYDJY4+bOvRxcazfctwGSmRMRdpRWi9bD4+gc4cCAegMMOBFpIf9vVsOqh6+CBGrCuz1xT5Ih3r23aw+0+QgCw7G2hErENITsHTIsNX1N7kdWv2ywanNwzTDcu9W2Sv+6IfWdh0so+qBXap3ccrK1UkgCQTFgk+NpoP7Jj6Y0PkGvGeH4eR6T+2vl3InpB9rojip3sohl4bEi58IxlzY+ih3wIY7K928RUJlYdOpEZteuSGVOYZqXM4vXW5ltTgkxrMIu5O2fjQHxIk5yhPfdfGKfYmF7xT+X+iSOTd1nG9pdbG/ihqo8EWtyPfwW8e13VpQrydIksHAu3MJ2hDJ98SKRfpw8l2/1TqRywzf8PxILE4omafdNpUv2KQ/loAJvkTGBiL2mFv5jKuRdkg8/+io7PnnYqn6qpOBLYN0kgb+Mr8ymsOhBuQ0KBUBUHaD9eS90r3s41H5Ta1XgvA1kqTVqpHXKMYBqqO3AgJZyIcu5hanAzejytsYnH0HLFxfeBKAiojkI1TOIf7lDfejn1SskylkyvTEM7D6GpXNKWPDkKv/crZ68UJT1RQ8wchF551IErEBPO7zWkjpudPECR85KhW4zPrjCNVgzYwTQnmPA6+cMKPKq1CE/OMvI++WZI8UojnxMfYl5+S9xUM+zFQaZOyi2YYdQHG+BPVvZUuDMlT2hdJUNG4avw8/SO3jjhW9TCJPZHv6C6cj+y0nC4/3Uq/bQZuxjbvH0CrtTc4eXXxPFl3ZSSSgTI6DQfpZMHvDcP8kqSQNUP2ac6Fk0BivsAHgzL8+d7jM/TYEuJWl2NUnvrSPxyF3ziR9CoGm60/IV3t9xzpaXzgtwK1450BwmA/ajPpIxsdAHNkW3MtnFwc3MZmFn75/DM3uAluHZtCSVFuhBNmrU2k8

On 30/09/2020 23:00, Agnishom Chattopadhyay wrote:
> Thank You. This is the version that finally worked:
>
> Definition list_nil_dec (l : list A) :
> {l = nil} + {l <> nil}.
> Proof.
> destruct l.
> - left. reflexivity.
> - right. discriminate.
> Qed.
>
> Fixpoint fromList' (l : list A) : (l <> nil) -> nonEmpty A.
> refine (match l with
> | nil => fun (H : nil <> nil) => _
> | (cons x xs) =>
> fun (_ : (cons x xs) <> nil) =>
> match (list_nil_dec xs) with
> | left _ => singleton x
> | right pr => consNE x (fromList' xs pr )
> end
> end).
> - exfalso. apply H. reflexivity.
> Defined.

I would add `abstract` before `discriminate`. This has the effect that
the sub-proof `x :: xs <> nil` is made opaque. Try `Print list_nil_dec`
to see the difference.

> I personally find the unguarded a bit mysterious. It seems like a
> limitation of Coq in not being able to see that a term is smaller than
> another.

I agree. ;-)

Re: [Coq-Club] Not enough information to resolve this refine goal, Maximilian Wuttke, 10/01/2020