# I don't know how to prove a simple theorem used with fixpoint in Coq

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
end.

Theorem t1 : forall i j : nat,
x i /\ f (S i) j <-> f i (S j).

• I feel like this question belongs to Stackoverflow because it is about getting the proof done and not about some concept of CS. – Anton Trunov Jun 7 '17 at 9:42
• 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! – Raphael Jun 9 '17 at 9:06
• Yeah, possibly. There'll be more of this in the future, so we should have a policy. – Andrej Bauer 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)
end.


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).
Proof.
destruct j.
- easy.
- induction j; firstorder; now rewrite Nat.add_succ_r in *.
Qed.


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
end.

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


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

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