The Coq mailing list

[Rui Baptista <rpgcbaptista AT gmail.com>]

If you can define it as a function, it should be possible and easier to define it as a relation.

Here's a proof of well founded induction that doesn't depend on Acc, and also another example of a function not structurally recursive on nat.

Axiom lt_0 : forall n1, n1 < 0 -> False.

Axiom lt_trans : forall n1 n2 n3, n1 < n2 -> n2 < S n3 -> n1 < n3.

Axiom ltb : nat -> nat -> bool.

Axiom ltb_minus : forall n1 n2, ltb n1 (S n2) = false -> n1 - S n2 < n1.

Definition nat_wf_rect : forall P1,

  (forall n1, (forall n2 : nat, n2 < n1 -> P1 n2) -> P1 n1) ->

  forall n1, P1 n1.

Proof.

refine (fun P1 H1 n1 => _).

refine (H1 _ _).

change ((fun n3 => forall n2, n2 < n3 -> P1 n2) n1).

refine (nat_rect _ _ _ _).

  refine (fun n2 H2 => _).

  refine (False_rect _ _).

  refine (lt_0 _ _).

  refine H2.

  refine (fun n2 H2 n3 H3 => _).

  refine (H1 _ _).

  refine (fun n4 H4 => _).

  refine (H2 _ _).

  refine (lt_trans _ _ _ _ _).

    refine H4.

    refine H3.

Defined.

Inductive div_rel : nat -> nat -> nat -> Prop :=

  | div_rel_0 : forall n1, div_rel n1 0 0

  | div_rel_ltb : forall n1 n2, ltb n1 (S n2) = true -> div_rel n1 (S n2) 0

  | div_rel_geb : forall n1 n2 n3, ltb n1 (S n2) = false ->

    div_rel (n1 - (S n2)) (S n2) n3 -> div_rel n1 (S n2) (S n3).

Definition div_strong : forall n1 n2, {n3 | div_rel n1 n2 n3}.

Proof.

refine (nat_wf_rect _ _).

refine (fun n1 H1 => _).

refine (nat_rect _ _ _).

  refine (exist _ _ _).

  refine (div_rel_0 _).

  refine (fun n2 H2 => _).

  refine ((_ : forall b1 : _, _ = b1 -> _) (ltb n1 (S n2)) eq_refl).

  refine (bool_rect _ _ _).

    refine (fun H3 => _).

    refine (exist _ _ _).

    refine (div_rel_ltb _ _ _).

    refine H3.

    refine (fun H3 => _).

    refine (_ (H1 _ _ _)).

      refine (sig_rect _ _).

      refine (fun n3 H4 => _).

      refine (exist _ _ _).

      refine (div_rel_geb _ _ _ _ _).

        refine H3.

        refine H4.

      refine (ltb_minus _ _ _).

      refine H3.

Defined.

Definition div : nat -> nat -> nat :=

  fun n1 n2 => proj1_sig (div_strong n1 n2).

On Sat, Nov 2, 2013 at 3:11 PM, Erik Silkensen <eriksilkensen AT gmail.com> wrote:

Ok, thanks.  I don’t know if this makes a difference, but anyway for context my goal is to define a step-indexed semantics in Coq where one of the rules looks kind of like

(forall k,

  k <= k’ ->

  eval term val k -> P) ->

-----------------------------

eval term val (S k')

so there’s a premise with a negative occurrence of eval.  I thought, if I can’t write this as an Inductive relation, maybe I could write it as a Fixpoint, where I could tell Coq k is the decreasing argument, and then that’s where I ran into wanting to recur with some k <= k’ and tried to extract that into the first code I sent.

On Nov 2, 2013, at 6:58 AM, Chris Dams <chris.dams.nl AT gmail.com> wrote:

Thanks for such a quick reply and for the pointer to well_founded_induction lt_wf.  Does this mean I should be using the Fix tactic?  Or Function or Program Fixpoint?  I think I’m getting stuck on how syntactically it should look for this basic example.  Thanks again.

I would not use fix or Fixpoint in that case. I would just apply well_founded_induction lt_wf by either using the apply tactic or providing it with arguments by typing them by hand.