Skip to main content
Proof Assistants Beta

Return to Answer

added 638 characters in body
Source Link
Feryll
Feryll
  • 214
  • 6

Also: You'll probably want to learn about thisthis if you haven't already, and end Cq_dec with Defined. rather than Qed. if you want to actually compute with delay.

Finally: Meven's solution is also fine, although I would recommend working with functions into Prop together with their decidability functions rather than functions into bool with their correctness theorems. One reason is that when destructing on the outputs of decidability functions, you automatically get the proposition or its negation added to your context, whereas if you work with bools, you will have to use the destruct ... eqn: ... variant and then manually apply your correctness theorems to get the same effect.

Also: You'll probably want to learn about this if you haven't already, and end Cq_dec with Defined. rather than Qed. if you want to actually compute with delay.

Also: You'll probably want to learn about this if you haven't already, and end Cq_dec with Defined. rather than Qed. if you want to actually compute with delay.

Finally: Meven's solution is also fine, although I would recommend working with functions into Prop together with their decidability functions rather than functions into bool with their correctness theorems. One reason is that when destructing on the outputs of decidability functions, you automatically get the proposition or its negation added to your context, whereas if you work with bools, you will have to use the destruct ... eqn: ... variant and then manually apply your correctness theorems to get the same effect.

Source Link
Feryll
Feryll
  • 214
  • 6

As others have said, the reason Coq does not accept your definition is that, although classical logic stipulates forall P, P \/ ~P, it is an undecidable (non-computable) problem to decide whether P or ~P holds for any given P.* Think about it: If RiemannHypothesis : Prop is an encoding of its namesake, how in your favorite programming language would you compute the value if RiemannHypothesis then 0 else 1? Or even worse, if ContinuumHypothesis then 0 else 1? :)

Luckily, P \/ ~P is decidable for many P that programmers actually care about. Equality of natural numbers is one of them (your T (S t)) = 0), and we must assume that your Cd is also decidable. Thus, your part of the exercise is to instantiate Cd_dec in the following, and you will have the definition of delay that you (truly) want.

Require Import Arith.

Variables Cd : nat -> nat -> Prop.
Variables T : nat -> nat.

(* This isn't possible to define for all nat -> nat -> Prop, but 
   presumably this is possible for Cd specifically. *)
Definition Cd_dec : forall n m, { Cd n m } + { ~Cd n m }.
Admitted.

Fixpoint delay (t:nat) {struct t} : nat :=
  match t with
  | 0 => 0
  | S t => if Nat.eq_dec (T (S t)) 0 then
            if Cd_dec ((S t) + (delay t) + 1 mod 2) (S t)
            then delay t + 1
            else delay t
           else delay t
  end.

I've taken the liberty of splitting the conjunction into a nested if. You can use && and coercions into bool to write it with the conjunction intact in only a single if, but I think you'll find this simpler to work with in practice.

Also: You'll probably want to learn about this if you haven't already, and end Cq_dec with Defined. rather than Qed. if you want to actually compute with delay.

* Because "P is true" in Coq better translates to "there exists a witness/proof of P," there are indeed propositions in base Coq for which neither it nor its negation has a witness.