wtf moment du jour, all guesses and comments welcome

Hi Gyesik and Matthieu,

Consider the following proof for your goal:

Theorem le_Pfact: forall x:nat, exists y, Pfact x y.
Proof.
fix circ 1.
intro.
destruct x.
exists 1.
constructor.
destruct x.
exists 1.
constructor.
pose proof (circ x) as H.
destruct H. (* existential var becomes x0 *)
exists (x * x0).
constructor.
assumption.
Save.

I find the above style of inductive proof much easier. Of course, the hypothesis "circ" must be applied in a well-founded way. However, there's no need to have an adequate induction principle readily available (or even bother to know what that induction principle should be).

Hope this helps,

Razvan

Matthieu Sozeau wrote:
{
{ Le 27 janv. 10 à 10:57, Gyesik Lee a écrit :
{
{{ Hi,
{}
} Hi Gyesik,
}
{{ as in the following case, an induction principle provided by Coq is sometimes not strong enough:
}}
{{ (A modified version of the example in Section 8.4.1.1 of CoqArt book.)
{{ ===================
{{ Open Scope nat_scope.
}}
{{ Inductive Pfact : nat -> nat -> Prop :=
{{ | Pfact0 : Pfact 0 1
{{ | Pfact1 : Pfact 1 1
{{ | Pfact2 : forall n v : nat, Pfact n v -> Pfact (S (S n)) (n * v).
}}
{{ Axiom lt_wf : well_founded lt.
}}
{{ Theorem le_Pfact : forall x : nat, exists y, Pfact x y.
{{ induction x.
{{ (* then the induction hypothesis is not strong enough*)
{{ Abort.
}}
{{ induction x using lt_wf.
{{ (* then the claim can be easily proved. *)
}}
{{ ===================
}}
{{ I am wondering if Coq provides a kind of mechanism producing the induction principle reflecting the well-foundedness of the canonically definable structural orderings on inductive types.
}
} My soon-to-be-released Equations [1] plugin has ML code to generate this order on any non-impredicative, computational inductive family (ie. most datatypes). You can derive both the subterm relation (actually the transitive closure of the direct subterm relation) and its wellfoundedness proof and a [Below] predicate that can be used to recurse and get a tuple
} of all the possible recursive calls in the context. You don't need to worry about guardness checks anymore if you use any of these, but you have to provide proofs that recursive arguments decrease in the first case or find your way in a tuple in the second case. This is partially automatable though.
}
} }}
}
} Require Import Equations.
}
} Open Scope nat_scope.
}
} Inductive Pfact : nat -> nat -> Prop :=
} | Pfact0 : Pfact 0 1
} | Pfact1 : Pfact 1 1
} | Pfact2 : forall n v : nat, Pfact n v -> Pfact (S (S n)) (n * v).
}
} Derive Subterm for nat.
}
} Theorem le_Pfact : forall x : nat, exists y, Pfact x y.
} apply FixWf; intros.
} destruct x. econstructor; constructor.
} destruct x. econstructor. constructor.
} destruct (H x). solve_rec.
} exists (x * x0). constructor; auto.
} Qed.
}
} Derive Below for nat.
}
} Definition rec_nat (P : nat -> Type) (step : Π n, Below_nat P n -> P
} n) n : P n :=
} step n (below_nat P step n).
}
} Theorem le_Pfact' : forall x : nat, exists y, Pfact x y.
} induction x using rec_nat.
} destruct x. econstructor; constructor.
} destruct x. econstructor. constructor.
} simpl in X. destruct_conjs.
} exists (x * e0). constructor; auto.
} Qed.
}
} }}
}
} [1] http://mattam.org/research/coq/equations.en.html
}
} -- Matthieu