The Coq mailing list

[Robin Green <greenrd AT greenrd.org>]

When the code fragment below is given to Coq (trunk version), the first
generated obligation is not provable (because it is false). Is this is
a bug in the obligation generating code?

More generally, how often should the obligation generator be expected to
generate provable obligations (assuming the overall goal is provable)?

--
Robin

---

Set Implicit Arguments. Unset Strict Implicit. Set Reversible Pattern
Implicit. Set Contextual Implicit.
Set Maximal Implicit Insertion.

(* A decidable proposition *)
Definition dec_Prop := { P : _ & { P } + { ~ P } }.

Require Import Program.Basics Program.Syntax List.
Open Scope program_scope.
Implicit Arguments projT1 [[A] [P]].
Implicit Arguments length [[A]].

(* How many of the propositions are true? *)
Definition count_truths := length ∘ flat_map (fun x : dec_Prop => if
projT2 x then [()] else []).

Section Prop_List.

  Variable lp : list Prop.

  (* Whether the given list is a decider list for lp *)
  Definition dec_for : list dec_Prop -> Prop := eq lp ∘ map projT1.

  Require Import Program.Tactics.
  (* Returns a proposition that is true iff at least one of the
elements of lp is true *)
  Program Definition any_of : { p : Prop |
forall ldp, dec_for ldp -> (p <-> count_truths ldp >= 1) }
    := match lp with
         cons h t => fold_left or t h
       | _ => False
       end.
    Next Obligation.

---

This is the state after "Next Obligation":

1 subgoal
lp : list Prop
h : Prop
t : list Prop
Heq_anonymous : h :: t = lp
x : Prop
H0 : forall ldp : list dec_Prop, dec_for ldp -> (x <-> count_truths ldp
>= 1) x0 : Prop
ldp : list dec_Prop
H : dec_for ldp
______________________________________(1/1)
x \/ x0 <-> count_truths ldp >= 1