Tagged Questions

5
votes
1answer
136 views

Are coinductive proofs necessary?

I've been exploring corecursion in Coq (specifically, infinite streams of natural numbers) lately and so far any coinductive predicate I've constructed and its coinductive proof can be transformed ...
1
vote
0answers
310 views

Consequences of technically proving anything in Coq (exploiting a bug)? [closed]

Technically, it is possible to prove anything in Coq proof assistant http ://coq.inria.fr due to a programming feature (or bug). This seems tractable when validating large proofs. Human analysis may ...