I am a beginner in coq and want to prove the following theorem t1. First I used induction i and destruct j, but it got bogged down in the middle. I would like some hints for this problem.

Function f takes two arguments of nat and returns Prop (e.g., f 2 4 = x 2 ∧ x 3 ∧ x 4 ∧ x 5).

Theorem t1 shows that a head of function f can be cut and concatenated (e.g., x 3 ∧ f 4 7 ⇔ f 3 8).

Parameter x : nat -> Prop.

Fixpoint f (o i : nat) : Prop :=
 match i with
 | S O =>  x (i+o-1)
 | S i' => f o i' /\ x (i+o-1)
 | _ => True

Theorem t1 : forall i j : nat, 
    x i /\ f (S i) j <-> f i (S j).
Proof. Admitted.
  • $\begingroup$ I feel like this question belongs to Stackoverflow because it is about getting the proof done and not about some concept of CS. $\endgroup$ Jun 7 '17 at 9:42
  • 1
    $\begingroup$ I tend to agree: this seems to be about using Coq, not the principles of using proof assistants (which would be ontopic, I guess). What's your take, @AndrejBauer? Community votes, please! $\endgroup$
    – Raphael
    Jun 9 '17 at 9:06
  • 2
    $\begingroup$ Yeah, possibly. There'll be more of this in the future, so we should have a policy. $\endgroup$ Jun 9 '17 at 9:27

First of all, let's simplify f just a little bit, keeping the special case when it doesn't let the trailing /\ True to appear in the generated proposition (I also renamed the parameter names to make them correspond to the ones used by the theorem below):

Fixpoint f' (i j : nat) : Prop :=
 match j with
 | 0 => True
 | 1 => x i
 | S j' => f' i j' /\ x (j' + i)

Now we can destruct j, take care of j = 0 case, then use induction on j again. Throwing in some automation we get the following:

Require Import Coq.Arith.Arith.

Theorem t1 : forall i j : nat,
  x i /\ f' (S i) j <-> f' i (S j).
  destruct j.
  - easy.
  - induction j; firstorder; now rewrite Nat.add_succ_r in *.

Notice that the structure of the proof mimics the definition of f': we treat the cases j = 0, j = 1 separately and then use the induction hypothesis (under the hood, firstorder does that) to prove the recursive case.


You are making your life difficult by defining things in convoluted ways. Here's how a better definition of the same thing makes the proof easy.

Fixpoint f_better n0 len : Prop :=
  match len with
  | 0 => True
  | S k => x n0 /\ f_better (S n0) k

Theorem t1_better: forall n0 len,
    x n0 /\ f_better (S n0) len <-> f_better n0 (S len).

If you really insist on using your version, we can prove that as well, but it'll be painful.

  • $\begingroup$ Thank you for adding a comment. I wasn't aware that f can be simplified to say so. $\endgroup$
    – FUJII S.
    Jun 7 '17 at 5:45

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.