Stuck on the proof of a simple Lemma: which induction should I use?
Question
I have the following structures:
Inductive instr : Set := | Select : nat -> instr | Backspace : instr. Definition prog := list instr.
and the following function:
Fixpoint Forward (input output : list nat) : option prog :=
match input with
| nil => match output with
| nil => Some nil
| y :: r => None
end
| x :: rest =>
match output with
| nil => match rest with
| nil => None
| xx :: rrest => match Forward rrest nil with
| Some pp => Some (Select x :: Backspace :: pp)
| None => None
end
end
| y :: r => if beq_nat x y then
match Forward rest r with
| Some pp => Some (Select x :: pp)
| None => None
end
else
match rest with
| nil => None
| xx :: rrest =>
match Forward rrest output with
| Some pp => Some (Select x :: Backspace :: pp)
| None => None
end
end
end
end.
Now I'd like to prove this simple Lemma:
forall (p p' : prog) (input1 input2 output : list nat),
Forward input1 output = Some p ->
Forward input2 nil = Some p' ->
Forward (input1 ++ input2) output = Some (p ++ p')
Note: As mentioned in the answer bellow, the more general form of the lemma is false:
forall (p p' : prog)
(input1 input2 output1 output2 : list nat),
Forward input1 output1 = Some p ->
Forward input2 output2 = Some p' ->
Forward (input1 ++ input2) (output1 ++ output2) =
Some (p ++ p')
Whatever induction principle I use, I'm stuck.
For example, I've tried this induction pattern:
A: Typeforall P : list A -> Prop, P nil -> (forall a : A, P (a :: nil)) -> (forall (a b : A) (tl : list A), P tl -> P (a :: b :: tl)) -> forall l : list A, P lA: Typeforall P : list A -> Prop, P nil -> (forall a : A, P (a :: nil)) -> (forall (a b : A) (tl : list A), P tl -> P (a :: b :: tl)) -> forall l : list A, P lA: Type
P: list A -> Prop
Pn: P nil
P1: forall a : A, P (a :: nil)
Prec: forall (a b : A) (tl : list A), P tl -> P (a :: b :: tl)forall l : list A, P lA: Type
P: list A -> Prop
Pn: P nil
P1: forall a : A, P (a :: nil)
Prec: forall (a b : A) (tl : list A), P tl -> P (a :: b :: tl)
tsli: forall l : list A, P lforall l : list A, P lA: Type
P: list A -> Prop
Pn: P nil
P1: forall a : A, P (a :: nil)
Prec: forall (a b : A) (tl : list A), P tl -> P (a :: b :: tl)
tsli: forall l : list A, P lP nilA: Type
P: list A -> Prop
Pn: P nil
P1: forall a : A, P (a :: nil)
Prec: forall (a b : A) (tl : list A), P tl -> P (a :: b :: tl)
tsli: forall l : list A, P l
x: A
l: list AP (x :: l)exact Pn.A: Type
P: list A -> Prop
Pn: P nil
P1: forall a : A, P (a :: nil)
Prec: forall (a b : A) (tl : list A), P tl -> P (a :: b :: tl)
tsli: forall l : list A, P lP nilA: Type
P: list A -> Prop
Pn: P nil
P1: forall a : A, P (a :: nil)
Prec: forall (a b : A) (tl : list A), P tl -> P (a :: b :: tl)
tsli: forall l : list A, P l
x: A
l: list AP (x :: l)A: Type
P: list A -> Prop
Pn: P nil
P1: forall a : A, P (a :: nil)
Prec: forall (a b : A) (tl : list A), P tl -> P (a :: b :: tl)
tsli: forall l : list A, P l
x: A
l: list AP l -> P (x :: l)A: Type
P: list A -> Prop
Pn: P nil
P1: forall a : A, P (a :: nil)
Prec: forall (a b : A) (tl : list A), P tl -> P (a :: b :: tl)
tsli: forall l : list A, P l
x: A
Pl: P nilP (x :: nil)A: Type
P: list A -> Prop
Pn: P nil
P1: forall a : A, P (a :: nil)
Prec: forall (a b : A) (tl : list A), P tl -> P (a :: b :: tl)
tsli: forall l : list A, P l
x, y: A
tl: list A
Pl: P (y :: tl)P (x :: y :: tl)exact (P1 x).A: Type
P: list A -> Prop
Pn: P nil
P1: forall a : A, P (a :: nil)
Prec: forall (a b : A) (tl : list A), P tl -> P (a :: b :: tl)
tsli: forall l : list A, P l
x: A
Pl: P nilP (x :: nil)A: Type
P: list A -> Prop
Pn: P nil
P1: forall a : A, P (a :: nil)
Prec: forall (a b : A) (tl : list A), P tl -> P (a :: b :: tl)
tsli: forall l : list A, P l
x, y: A
tl: list A
Pl: P (y :: tl)P (x :: y :: tl)exact (tsli tl). Defined.A: Type
P: list A -> Prop
Pn: P nil
P1: forall a : A, P (a :: nil)
Prec: forall (a b : A) (tl : list A), P tl -> P (a :: b :: tl)
tsli: forall l : list A, P l
x, y: A
tl: list A
Pl: P (y :: tl)P tl
But I didn't manage to finalize the proof. There must be something obvious I don't see. Can't someone help me with this proof?
Answer
There are two problems with your question. The first one is that the statement you want to prove is false, here is a proof of a counter example.
~ (forall (p p' : prog) (input1 input2 output1 output2 : list nat), Forward input1 output1 = Some p -> Forward input2 output2 = Some p' -> Forward (input1 ++ input2) (output1 ++ output2) = Some (p ++ p'))~ (forall (p p' : prog) (input1 input2 output1 output2 : list nat), Forward input1 output1 = Some p -> Forward input2 output2 = Some p' -> Forward (input1 ++ input2) (output1 ++ output2) = Some (p ++ p'))abs: forall (p p' : prog) (input1 input2 output1 output2 : list nat), Forward input1 output1 = Some p -> Forward input2 output2 = Some p' -> Forward (input1 ++ input2) (output1 ++ output2) = Some (p ++ p')Falseabs: forall (p p' : prog) (input1 input2 output1 output2 : list nat), Forward input1 output1 = Some p -> Forward input2 output2 = Some p' -> Forward (input1 ++ input2) (output1 ++ output2) = Some (p ++ p')
tmp: Forward ((1 :: 2 :: nil) ++ 1 :: 2 :: nil) (nil ++ 1 :: 2 :: nil) = Some ((Select 1 :: Backspace :: nil) ++ Select 1 :: Select 2 :: nil)Falsediscriminate. Qed.abs: forall (p p' : prog) (input1 input2 output1 output2 : list nat), Forward input1 output1 = Some p -> Forward input2 output2 = Some p' -> Forward (input1 ++ input2) (output1 ++ output2) = Some (p ++ p')
tmp: Some (Select 1 :: Select 2 :: Select 1 :: Backspace :: nil) = Some (Select 1 :: Backspace :: Select 1 :: Select 2 :: nil)False
So, contrary to your claim, this is not a simple lemma.
The second problem is that the function has a complicated shape and the proof by induction is difficult to organize. I cover this aspect just below.
From the structure of the function Forward, it is natural that you should perform your proof by induction over the input argument, because it is the argument where recursive calls occur on a subterm. However the proof is made complicated by the fact that recursive calls happen not only on direct subterms (as in Forward rest ...) but also in subterms of subterms (as in Forward rrest ...).
There are several ways out of this difficulty, but all require some amount of explanation or learning.
One way is to use the Equations plugin to Coq and redefine your Forward function using Equations. You can then use functional induction to solve your problem: this will use an induction principle that especially tailored to your problem.
A second way is to build a tailored induction principle by hand. Here is an attempt.
A: Typeforall P : list A -> Prop, P nil -> (forall a : A, P (a :: nil)) -> (forall (a b : A) (tl : list A), P (b :: tl) -> P tl -> P (a :: b :: tl)) -> forall l : list A, P lA: Typeforall P : list A -> Prop, P nil -> (forall a : A, P (a :: nil)) -> (forall (a b : A) (tl : list A), P (b :: tl) -> P tl -> P (a :: b :: tl)) -> forall l : list A, P lA: Type
P: list A -> Prop
Pn: P nil
P1: forall a : A, P (a :: nil)
Prec: forall (a b : A) (tl : list A), P (b :: tl) -> P tl -> P (a :: b :: tl)forall l : list A, P lA: Type
P: list A -> Prop
Pn: P nil
P1: forall a : A, P (a :: nil)
Prec: forall (a b : A) (tl : list A), P (b :: tl) -> P tl -> P (a :: b :: tl)
tsli: forall l : list A, P lforall l : list A, P lA: Type
P: list A -> Prop
Pn: P nil
P1: forall a : A, P (a :: nil)
Prec: forall (a b : A) (tl : list A), P (b :: tl) -> P tl -> P (a :: b :: tl)
tsli: forall l : list A, P lP nilA: Type
P: list A -> Prop
Pn: P nil
P1: forall a : A, P (a :: nil)
Prec: forall (a b : A) (tl : list A), P (b :: tl) -> P tl -> P (a :: b :: tl)
tsli: forall l : list A, P l
x: A
l: list AP (x :: l)exact Pn.A: Type
P: list A -> Prop
Pn: P nil
P1: forall a : A, P (a :: nil)
Prec: forall (a b : A) (tl : list A), P (b :: tl) -> P tl -> P (a :: b :: tl)
tsli: forall l : list A, P lP nilA: Type
P: list A -> Prop
Pn: P nil
P1: forall a : A, P (a :: nil)
Prec: forall (a b : A) (tl : list A), P (b :: tl) -> P tl -> P (a :: b :: tl)
tsli: forall l : list A, P l
x: A
l: list AP (x :: l)A: Type
P: list A -> Prop
Pn: P nil
P1: forall a : A, P (a :: nil)
Prec: forall (a b : A) (tl : list A), P (b :: tl) -> P tl -> P (a :: b :: tl)
tsli: forall l : list A, P l
x: A
l: list AP l -> P (x :: l)A: Type
P: list A -> Prop
Pn: P nil
P1: forall a : A, P (a :: nil)
Prec: forall (a b : A) (tl : list A), P (b :: tl) -> P tl -> P (a :: b :: tl)
tsli: forall l : list A, P l
x: A
Pl: P nilP (x :: nil)A: Type
P: list A -> Prop
Pn: P nil
P1: forall a : A, P (a :: nil)
Prec: forall (a b : A) (tl : list A), P (b :: tl) -> P tl -> P (a :: b :: tl)
tsli: forall l : list A, P l
x, y: A
tl: list A
Pl: P (y :: tl)P (x :: y :: tl)exact (P1 x).A: Type
P: list A -> Prop
Pn: P nil
P1: forall a : A, P (a :: nil)
Prec: forall (a b : A) (tl : list A), P (b :: tl) -> P tl -> P (a :: b :: tl)
tsli: forall l : list A, P l
x: A
Pl: P nilP (x :: nil)apply Prec; [assumption | exact (tsli tl)]. Defined.A: Type
P: list A -> Prop
Pn: P nil
P1: forall a : A, P (a :: nil)
Prec: forall (a b : A) (tl : list A), P (b :: tl) -> P tl -> P (a :: b :: tl)
tsli: forall l : list A, P l
x, y: A
tl: list A
Pl: P (y :: tl)P (x :: y :: tl)You can then start your proof with a command of the following shape:
forall (p p' : prog) (input1 input2 output1 output2 : list nat), Forward input1 output1 = Some p -> Forward input2 output2 = Some p' -> Forward (input1 ++ input2) (output1 ++ output2) = Some (p ++ p')forall (p p' : prog) (input1 input2 output1 output2 : list nat), Forward input1 output1 = Some p -> Forward input2 output2 = Some p' -> Forward (input1 ++ input2) (output1 ++ output2) = Some (p ++ p')p, p': prog
input1: list natforall input2 output1 output2 : list nat, Forward input1 output1 = Some p -> Forward input2 output2 = Some p' -> Forward (input1 ++ input2) (output1 ++ output2) = Some (p ++ p')p': prog
input1: list natforall (p : prog) (input2 output1 output2 : list nat), Forward input1 output1 = Some p -> Forward input2 output2 = Some p' -> Forward (input1 ++ input2) (output1 ++ output2) = Some (p ++ p')p': progforall (p : prog) (input2 output1 output2 : list nat), Forward nil output1 = Some p -> Forward input2 output2 = Some p' -> Forward (nil ++ input2) (output1 ++ output2) = Some (p ++ p')p': prog
a: natforall (p : prog) (input2 output1 output2 : list nat), Forward (a :: nil) output1 = Some p -> Forward input2 output2 = Some p' -> Forward ((a :: nil) ++ input2) (output1 ++ output2) = Some (p ++ p')p': prog
a, b: nat
tl: list nat
Ih1: forall (p : prog) (input2 output1 output2 : list nat), Forward (b :: tl) output1 = Some p -> Forward input2 output2 = Some p' -> Forward ((b :: tl) ++ input2) (output1 ++ output2) = Some (p ++ p')
Ih2: forall (p : prog) (input2 output1 output2 : list nat), Forward tl output1 = Some p -> Forward input2 output2 = Some p' -> Forward (tl ++ input2) (output1 ++ output2) = Some (p ++ p')forall (p : prog) (input2 output1 output2 : list nat), Forward (a :: b :: tl) output1 = Some p -> Forward input2 output2 = Some p' -> Forward ((a :: b :: tl) ++ input2) (output1 ++ output2) = Some (p ++ p')But, as I already said, the lemma you want to prove is actually false, so there is no way this proof will ever work and I cannot illustrate that the proposed approach is going to work.
EDIT: Now that the original question has been corrected, here is a full correction to the original question:
forall (p p' : prog) (input1 input2 output : list nat), Forward input1 output = Some p -> Forward input2 nil = Some p' -> Forward (input1 ++ input2) output = Some (p ++ p')forall (p p' : prog) (input1 input2 output : list nat), Forward input1 output = Some p -> Forward input2 nil = Some p' -> Forward (input1 ++ input2) output = Some (p ++ p')p, p': prog
input1: list natforall input2 output : list nat, Forward input1 output = Some p -> Forward input2 nil = Some p' -> Forward (input1 ++ input2) output = Some (p ++ p')p': prog
input1: list natforall (p : prog) (input2 output : list nat), Forward input1 output = Some p -> Forward input2 nil = Some p' -> Forward (input1 ++ input2) output = Some (p ++ p')p': progforall (p : prog) (input2 output : list nat), Forward nil output = Some p -> Forward input2 nil = Some p' -> Forward (nil ++ input2) output = Some (p ++ p')p': prog
x: natforall (p : prog) (input2 output : list nat), Forward (x :: nil) output = Some p -> Forward input2 nil = Some p' -> Forward ((x :: nil) ++ input2) output = Some (p ++ p')p': prog
x, xx: nat
rrest: list nat
Ih1: forall (p : prog) (input2 output : list nat), Forward (xx :: rrest) output = Some p -> Forward input2 nil = Some p' -> Forward ((xx :: rrest) ++ input2) output = Some (p ++ p')
Ih2: forall (p : prog) (input2 output : list nat), Forward rrest output = Some p -> Forward input2 nil = Some p' -> Forward (rrest ++ input2) output = Some (p ++ p')forall (p : prog) (input2 output : list nat), Forward (x :: xx :: rrest) output = Some p -> Forward input2 nil = Some p' -> Forward ((x :: xx :: rrest) ++ input2) output = Some (p ++ p')p': progforall (p : prog) (input2 output : list nat), Forward nil output = Some p -> Forward input2 nil = Some p' -> Forward (nil ++ input2) output = Some (p ++ p')p': progforall (p : prog) (input2 output : list nat), match output with | nil => Some nil | _ :: _ => None end = Some p -> Forward input2 nil = Some p' -> Forward input2 output = Some (p ++ p')p', p: prog
input2: list natSome nil = Some p -> Forward input2 nil = Some p' -> Forward input2 nil = Some (p ++ p')p', p: prog
input2: list nat
no1: nat
output: list natNone = Some p -> Forward input2 nil = Some p' -> Forward input2 (no1 :: output) = Some (p ++ p')p', p: prog
input2: list natSome nil = Some p -> Forward input2 nil = Some p' -> Forward input2 nil = Some (p ++ p')p', p: prog
input2: list nat
p_is_nil: nil = pForward input2 nil = Some p' -> Forward input2 nil = Some (p ++ p')p', p: prog
input2: list nat
p_is_nil: nil = pForward input2 nil = Some p' -> Forward input2 nil = Some (nil ++ p')auto.p', p: prog
input2: list nat
p_is_nil: nil = pForward input2 nil = Some p' -> Forward input2 nil = Some p'discriminate.p', p: prog
input2: list nat
no1: nat
output: list natNone = Some p -> Forward input2 nil = Some p' -> Forward input2 (no1 :: output) = Some (p ++ p')p': prog
x: natforall (p : prog) (input2 output : list nat), Forward (x :: nil) output = Some p -> Forward input2 nil = Some p' -> Forward ((x :: nil) ++ input2) output = Some (p ++ p')p': prog
x: natforall (p : prog) (input2 output : list nat), match output with | nil => None | y :: r => if x =? y then match match r with | nil => Some nil | _ :: _ => None end with | Some pp => Some (Select x :: pp) | None => None end else None end = Some p -> Forward input2 nil = Some p' -> match output with | nil => match input2 with | nil => None | _ :: rrest => match Forward rrest nil with | Some pp => Some (Select x :: Backspace :: pp) | None => None end end | y :: r => if x =? y then match Forward input2 r with | Some pp => Some (Select x :: pp) | None => None end else match input2 with | nil => None | _ :: rrest => match Forward rrest output with | Some pp => Some (Select x :: Backspace :: pp) | None => None end end end = Some (p ++ p')p': prog
x: nat
p: prog
input2: list nat
y: nat
r: list nat(if x =? y then match match r with | nil => Some nil | _ :: _ => None end with | Some pp => Some (Select x :: pp) | None => None end else None) = Some p -> Forward input2 nil = Some p' -> (if x =? y then match Forward input2 r with | Some pp => Some (Select x :: pp) | None => None end else match input2 with | nil => None | _ :: rrest => match Forward rrest (y :: r) with | Some pp => Some (Select x :: Backspace :: pp) | None => None end end) = Some (p ++ p')p': prog
x: nat
p: prog
input2: list nat
y: nat
r: list natmatch match r with | nil => Some nil | _ :: _ => None end with | Some pp => Some (Select x :: pp) | None => None end = Some p -> Forward input2 nil = Some p' -> match Forward input2 r with | Some pp => Some (Select x :: pp) | None => None end = Some (p ++ p')now intros [= pval] v2; rewrite <- pval, v2; simpl.p': prog
x: nat
p: prog
input2: list nat
y: natSome (Select x :: nil) = Some p -> Forward input2 nil = Some p' -> match Forward input2 nil with | Some pp => Some (Select x :: pp) | None => None end = Some (p ++ p')p': prog
x, xx: nat
rrest: list nat
Ih1: forall (p : prog) (input2 output : list nat), Forward (xx :: rrest) output = Some p -> Forward input2 nil = Some p' -> Forward ((xx :: rrest) ++ input2) output = Some (p ++ p')
Ih2: forall (p : prog) (input2 output : list nat), Forward rrest output = Some p -> Forward input2 nil = Some p' -> Forward (rrest ++ input2) output = Some (p ++ p')forall (p : prog) (input2 output : list nat), Forward (x :: xx :: rrest) output = Some p -> Forward input2 nil = Some p' -> Forward ((x :: xx :: rrest) ++ input2) output = Some (p ++ p')p': prog
x, xx: nat
rrest: list nat
Ih1: forall (p : prog) (input2 output : list nat), Forward (xx :: rrest) output = Some p -> Forward input2 nil = Some p' -> Forward ((xx :: rrest) ++ input2) output = Some (p ++ p')
Ih2: forall (p : prog) (input2 output : list nat), Forward rrest output = Some p -> Forward input2 nil = Some p' -> Forward (rrest ++ input2) output = Some (p ++ p')
p: prog
input2, output: list natForward (x :: xx :: rrest) output = Some p -> Forward input2 nil = Some p' -> Forward ((x :: xx :: rrest) ++ input2) output = Some (p ++ p')p': prog
x, xx: nat
rrest: list nat
Ih1: forall (p : prog) (input2 output : list nat), Forward (xx :: rrest) output = Some p -> Forward input2 nil = Some p' -> Forward ((xx :: rrest) ++ input2) output = Some (p ++ p')
Ih2: forall (p : prog) (input2 output : list nat), Forward rrest output = Some p -> Forward input2 nil = Some p' -> Forward (rrest ++ input2) output = Some (p ++ p')
p: prog
input2: list natForward (x :: xx :: rrest) nil = Some p -> Forward input2 nil = Some p' -> Forward ((x :: xx :: rrest) ++ input2) nil = Some (p ++ p')p': prog
x, xx: nat
rrest: list nat
Ih1: forall (p : prog) (input2 output : list nat), Forward (xx :: rrest) output = Some p -> Forward input2 nil = Some p' -> Forward ((xx :: rrest) ++ input2) output = Some (p ++ p')
Ih2: forall (p : prog) (input2 output : list nat), Forward rrest output = Some p -> Forward input2 nil = Some p' -> Forward (rrest ++ input2) output = Some (p ++ p')
p: prog
input2: list nat
y: nat
r: list natForward (x :: xx :: rrest) (y :: r) = Some p -> Forward input2 nil = Some p' -> Forward ((x :: xx :: rrest) ++ input2) (y :: r) = Some (p ++ p')p': prog
x, xx: nat
rrest: list nat
Ih1: forall (p : prog) (input2 output : list nat), Forward (xx :: rrest) output = Some p -> Forward input2 nil = Some p' -> Forward ((xx :: rrest) ++ input2) output = Some (p ++ p')
Ih2: forall (p : prog) (input2 output : list nat), Forward rrest output = Some p -> Forward input2 nil = Some p' -> Forward (rrest ++ input2) output = Some (p ++ p')
p: prog
input2: list natForward (x :: xx :: rrest) nil = Some p -> Forward input2 nil = Some p' -> Forward ((x :: xx :: rrest) ++ input2) nil = Some (p ++ p')p': prog
x, xx: nat
rrest: list nat
Ih1: forall (p : prog) (input2 output : list nat), Forward (xx :: rrest) output = Some p -> Forward input2 nil = Some p' -> Forward ((xx :: rrest) ++ input2) output = Some (p ++ p')
Ih2: forall (p : prog) (input2 output : list nat), Forward rrest output = Some p -> Forward input2 nil = Some p' -> Forward (rrest ++ input2) output = Some (p ++ p')
p: prog
input2: list natmatch Forward rrest nil with | Some pp => Some (Select x :: Backspace :: pp) | None => None end = Some p -> Forward input2 nil = Some p' -> Forward ((x :: xx :: rrest) ++ input2) nil = Some (p ++ p')p': prog
x, xx: nat
rrest: list nat
Ih1: forall (p : prog) (input2 output : list nat), Forward (xx :: rrest) output = Some p -> Forward input2 nil = Some p' -> Forward ((xx :: rrest) ++ input2) output = Some (p ++ p')
Ih2: forall (p : prog) (input2 output : list nat), Forward rrest output = Some p -> Forward input2 nil = Some p' -> Forward (rrest ++ input2) output = Some (p ++ p')
p: prog
input2: list nat
v: prog
vtl: Forward rrest nil = Some vSome (Select x :: Backspace :: v) = Some p -> Forward input2 nil = Some p' -> Forward ((x :: xx :: rrest) ++ input2) nil = Some (p ++ p')p': prog
x, xx: nat
rrest: list nat
Ih1: forall (p : prog) (input2 output : list nat), Forward (xx :: rrest) output = Some p -> Forward input2 nil = Some p' -> Forward ((xx :: rrest) ++ input2) output = Some (p ++ p')
Ih2: forall (p : prog) (input2 output : list nat), Forward rrest output = Some p -> Forward input2 nil = Some p' -> Forward (rrest ++ input2) output = Some (p ++ p')
p: prog
input2: list nat
v: prog
vtl: Forward rrest nil = Some v
pval: Select x :: Backspace :: v = p
p'val: Forward input2 nil = Some p'Forward ((x :: xx :: rrest) ++ input2) nil = Some (p ++ p')p': prog
x, xx: nat
rrest: list nat
Ih1: forall (p : prog) (input2 output : list nat), Forward (xx :: rrest) output = Some p -> Forward input2 nil = Some p' -> Forward ((xx :: rrest) ++ input2) output = Some (p ++ p')
Ih2: forall (p : prog) (input2 output : list nat), Forward rrest output = Some p -> Forward input2 nil = Some p' -> Forward (rrest ++ input2) output = Some (p ++ p')
p: prog
input2: list nat
v: prog
vtl: Forward rrest nil = Some v
pval: Select x :: Backspace :: v = p
p'val: Forward input2 nil = Some p'
tmp: Forward (rrest ++ input2) nil = Some (v ++ p')Forward ((x :: xx :: rrest) ++ input2) nil = Some (p ++ p')p': prog
x, xx: nat
rrest: list nat
Ih1: forall (p : prog) (input2 output : list nat), Forward (xx :: rrest) output = Some p -> Forward input2 nil = Some p' -> Forward ((xx :: rrest) ++ input2) output = Some (p ++ p')
Ih2: forall (p : prog) (input2 output : list nat), Forward rrest output = Some p -> Forward input2 nil = Some p' -> Forward (rrest ++ input2) output = Some (p ++ p')
p: prog
input2: list nat
v: prog
vtl: Forward rrest nil = Some v
pval: Select x :: Backspace :: v = p
p'val: Forward input2 nil = Some p'
tmp: Forward (rrest ++ input2) nil = Some (v ++ p')match Forward (rrest ++ input2) nil with | Some pp => Some (Select x :: Backspace :: pp) | None => None end = Some (p ++ p')easy.p': prog
x, xx: nat
rrest: list nat
Ih1: forall (p : prog) (input2 output : list nat), Forward (xx :: rrest) output = Some p -> Forward input2 nil = Some p' -> Forward ((xx :: rrest) ++ input2) output = Some (p ++ p')
Ih2: forall (p : prog) (input2 output : list nat), Forward rrest output = Some p -> Forward input2 nil = Some p' -> Forward (rrest ++ input2) output = Some (p ++ p')
p: prog
input2: list nat
v: prog
vtl: Forward rrest nil = Some v
pval: Select x :: Backspace :: v = p
p'val: Forward input2 nil = Some p'
tmp: Forward (rrest ++ input2) nil = Some (v ++ p')Some (Select x :: Backspace :: v ++ p') = Some ((Select x :: Backspace :: v) ++ p')p': prog
x, xx: nat
rrest: list nat
Ih1: forall (p : prog) (input2 output : list nat), Forward (xx :: rrest) output = Some p -> Forward input2 nil = Some p' -> Forward ((xx :: rrest) ++ input2) output = Some (p ++ p')
Ih2: forall (p : prog) (input2 output : list nat), Forward rrest output = Some p -> Forward input2 nil = Some p' -> Forward (rrest ++ input2) output = Some (p ++ p')
p: prog
input2: list nat
y: nat
r: list natForward (x :: xx :: rrest) (y :: r) = Some p -> Forward input2 nil = Some p' -> Forward ((x :: xx :: rrest) ++ input2) (y :: r) = Some (p ++ p')p': prog
x, xx: nat
rrest: list nat
Ih1: forall (p : prog) (input2 output : list nat), Forward (xx :: rrest) output = Some p -> Forward input2 nil = Some p' -> Forward ((xx :: rrest) ++ input2) output = Some (p ++ p')
Ih2: forall (p : prog) (input2 output : list nat), Forward rrest output = Some p -> Forward input2 nil = Some p' -> Forward (rrest ++ input2) output = Some (p ++ p')
p: prog
input2: list nat
y: nat
r: list nat(if x =? y then match Forward (xx :: rrest) r with | Some pp => Some (Select x :: pp) | None => None end else match Forward rrest (y :: r) with | Some pp => Some (Select x :: Backspace :: pp) | None => None end) = Some p -> Forward input2 nil = Some p' -> Forward ((x :: xx :: rrest) ++ input2) (y :: r) = Some (p ++ p')p': prog
x, xx: nat
rrest: list nat
Ih1: forall (p : prog) (input2 output : list nat), Forward (xx :: rrest) output = Some p -> Forward input2 nil = Some p' -> Forward ((xx :: rrest) ++ input2) output = Some (p ++ p')
Ih2: forall (p : prog) (input2 output : list nat), Forward rrest output = Some p -> Forward input2 nil = Some p' -> Forward (rrest ++ input2) output = Some (p ++ p')
p: prog
input2: list nat
y: nat
r: list nat
vrest: prog
eqnrest: Forward (xx :: rrest) r = Some vrest(if x =? y then Some (Select x :: vrest) else match Forward rrest (y :: r) with | Some pp => Some (Select x :: Backspace :: pp) | None => None end) = Some p -> Forward input2 nil = Some p' -> Forward ((x :: xx :: rrest) ++ input2) (y :: r) = Some (p ++ p')p': prog
x, xx: nat
rrest: list nat
Ih1: forall (p : prog) (input2 output : list nat), Forward (xx :: rrest) output = Some p -> Forward input2 nil = Some p' -> Forward ((xx :: rrest) ++ input2) output = Some (p ++ p')
Ih2: forall (p : prog) (input2 output : list nat), Forward rrest output = Some p -> Forward input2 nil = Some p' -> Forward (rrest ++ input2) output = Some (p ++ p')
p: prog
input2: list nat
y: nat
r: list nat
eqnrest: Forward (xx :: rrest) r = None(if x =? y then None else match Forward rrest (y :: r) with | Some pp => Some (Select x :: Backspace :: pp) | None => None end) = Some p -> Forward input2 nil = Some p' -> Forward ((x :: xx :: rrest) ++ input2) (y :: r) = Some (p ++ p')p': prog
x, xx: nat
rrest: list nat
Ih1: forall (p : prog) (input2 output : list nat), Forward (xx :: rrest) output = Some p -> Forward input2 nil = Some p' -> Forward ((xx :: rrest) ++ input2) output = Some (p ++ p')
Ih2: forall (p : prog) (input2 output : list nat), Forward rrest output = Some p -> Forward input2 nil = Some p' -> Forward (rrest ++ input2) output = Some (p ++ p')
p: prog
input2: list nat
y: nat
r: list nat
vrest: prog
eqnrest: Forward (xx :: rrest) r = Some vrest(if x =? y then Some (Select x :: vrest) else match Forward rrest (y :: r) with | Some pp => Some (Select x :: Backspace :: pp) | None => None end) = Some p -> Forward input2 nil = Some p' -> Forward ((x :: xx :: rrest) ++ input2) (y :: r) = Some (p ++ p')p': prog
x, xx: nat
rrest: list nat
Ih1: forall (p : prog) (input2 output : list nat), Forward (xx :: rrest) output = Some p -> Forward input2 nil = Some p' -> Forward ((xx :: rrest) ++ input2) output = Some (p ++ p')
Ih2: forall (p : prog) (input2 output : list nat), Forward rrest output = Some p -> Forward input2 nil = Some p' -> Forward (rrest ++ input2) output = Some (p ++ p')
p: prog
input2: list nat
y: nat
r: list nat
vrest: prog
eqnrest: Forward (xx :: rrest) r = Some vrest
xeqy: (x =? y) = trueSome (Select x :: vrest) = Some p -> Forward input2 nil = Some p' -> Forward ((x :: xx :: rrest) ++ input2) (y :: r) = Some (p ++ p')p': prog
x, xx: nat
rrest: list nat
Ih1: forall (p : prog) (input2 output : list nat), Forward (xx :: rrest) output = Some p -> Forward input2 nil = Some p' -> Forward ((xx :: rrest) ++ input2) output = Some (p ++ p')
Ih2: forall (p : prog) (input2 output : list nat), Forward rrest output = Some p -> Forward input2 nil = Some p' -> Forward (rrest ++ input2) output = Some (p ++ p')
p: prog
input2: list nat
y: nat
r: list nat
vrest: prog
eqnrest: Forward (xx :: rrest) r = Some vrest
xeqy: (x =? y) = falsematch Forward rrest (y :: r) with | Some pp => Some (Select x :: Backspace :: pp) | None => None end = Some p -> Forward input2 nil = Some p' -> Forward ((x :: xx :: rrest) ++ input2) (y :: r) = Some (p ++ p')p': prog
x, xx: nat
rrest: list nat
Ih1: forall (p : prog) (input2 output : list nat), Forward (xx :: rrest) output = Some p -> Forward input2 nil = Some p' -> Forward ((xx :: rrest) ++ input2) output = Some (p ++ p')
Ih2: forall (p : prog) (input2 output : list nat), Forward rrest output = Some p -> Forward input2 nil = Some p' -> Forward (rrest ++ input2) output = Some (p ++ p')
p: prog
input2: list nat
y: nat
r: list nat
vrest: prog
eqnrest: Forward (xx :: rrest) r = Some vrest
xeqy: (x =? y) = trueSome (Select x :: vrest) = Some p -> Forward input2 nil = Some p' -> Forward ((x :: xx :: rrest) ++ input2) (y :: r) = Some (p ++ p')p': prog
x, xx: nat
rrest: list nat
Ih1: forall (p : prog) (input2 output : list nat), Forward (xx :: rrest) output = Some p -> Forward input2 nil = Some p' -> Forward ((xx :: rrest) ++ input2) output = Some (p ++ p')
Ih2: forall (p : prog) (input2 output : list nat), Forward rrest output = Some p -> Forward input2 nil = Some p' -> Forward (rrest ++ input2) output = Some (p ++ p')
p: prog
input2: list nat
y: nat
r: list nat
vrest: prog
eqnrest: Forward (xx :: rrest) r = Some vrest
xeqy: (x =? y) = true
vp: Select x :: vrest = p
v2: Forward input2 nil = Some p'Forward ((x :: xx :: rrest) ++ input2) (y :: r) = Some (p ++ p')p': prog
x, xx: nat
rrest: list nat
Ih1: forall (p : prog) (input2 output : list nat), Forward (xx :: rrest) output = Some p -> Forward input2 nil = Some p' -> Forward ((xx :: rrest) ++ input2) output = Some (p ++ p')
Ih2: forall (p : prog) (input2 output : list nat), Forward rrest output = Some p -> Forward input2 nil = Some p' -> Forward (rrest ++ input2) output = Some (p ++ p')
p: prog
input2: list nat
y: nat
r: list nat
vrest: prog
eqnrest: Forward (xx :: rrest) r = Some vrest
xeqy: (x =? y) = true
vp: Select x :: vrest = p
v2: Forward input2 nil = Some p'Forward ((x :: xx :: rrest) ++ input2) (y :: r) = Some ((Select x :: vrest) ++ p')p': prog
x, xx: nat
rrest: list nat
Ih1: forall (p : prog) (input2 output : list nat), Forward (xx :: rrest) output = Some p -> Forward input2 nil = Some p' -> Forward ((xx :: rrest) ++ input2) output = Some (p ++ p')
Ih2: forall (p : prog) (input2 output : list nat), Forward rrest output = Some p -> Forward input2 nil = Some p' -> Forward (rrest ++ input2) output = Some (p ++ p')
p: prog
input2: list nat
y: nat
r: list nat
vrest: prog
eqnrest: Forward (xx :: rrest) r = Some vrest
xeqy: (x =? y) = true
v2: Forward input2 nil = Some p'Forward ((x :: xx :: rrest) ++ input2) (y :: r) = Some ((Select x :: vrest) ++ p')p': prog
x, xx: nat
rrest: list nat
Ih1: forall (p : prog) (input2 output : list nat), Forward (xx :: rrest) output = Some p -> Forward input2 nil = Some p' -> Forward ((xx :: rrest) ++ input2) output = Some (p ++ p')
Ih2: forall (p : prog) (input2 output : list nat), Forward rrest output = Some p -> Forward input2 nil = Some p' -> Forward (rrest ++ input2) output = Some (p ++ p')
p: prog
input2: list nat
y: nat
r: list nat
vrest: prog
eqnrest: Forward (xx :: rrest) r = Some vrest
xeqy: (x =? y) = true
v2: Forward input2 nil = Some p'Forward ((xx :: rrest) ++ input2) r = Some (vrest ++ p') -> Forward ((x :: xx :: rrest) ++ input2) (y :: r) = Some ((Select x :: vrest) ++ p')p': prog
x, xx: nat
rrest: list nat
Ih1: forall (p : prog) (input2 output : list nat), Forward (xx :: rrest) output = Some p -> Forward input2 nil = Some p' -> Forward ((xx :: rrest) ++ input2) output = Some (p ++ p')
Ih2: forall (p : prog) (input2 output : list nat), Forward rrest output = Some p -> Forward input2 nil = Some p' -> Forward (rrest ++ input2) output = Some (p ++ p')
p: prog
input2: list nat
y: nat
r: list nat
vrest: prog
eqnrest: Forward (xx :: rrest) r = Some vrest
xeqy: (x =? y) = true
v2: Forward input2 nil = Some p'match r with | nil => match rrest ++ input2 with | nil => None | _ :: rrest => match Forward rrest nil with | Some pp => Some (Select xx :: Backspace :: pp) | None => None end end | y :: r0 => if xx =? y then match Forward (rrest ++ input2) r0 with | Some pp => Some (Select xx :: pp) | None => None end else match rrest ++ input2 with | nil => None | _ :: rrest => match Forward rrest r with | Some pp => Some (Select xx :: Backspace :: pp) | None => None end end end = Some (vrest ++ p') -> (if x =? y then match match r with | nil => match rrest ++ input2 with | nil => None | _ :: rrest => match Forward rrest nil with | Some pp => Some (Select xx :: Backspace :: pp) | None => None end end | y :: r0 => if xx =? y then match Forward (rrest ++ input2) r0 with | Some pp => Some (Select xx :: pp) | None => None end else match rrest ++ input2 with | nil => None | _ :: rrest => match Forward rrest r with | Some pp => Some (Select xx :: Backspace :: pp) | None => None end end end with | Some pp => Some (Select x :: pp) | None => None end else match Forward (rrest ++ input2) (y :: r) with | Some pp => Some (Select x :: Backspace :: pp) | None => None end) = Some (Select x :: vrest ++ p')p': prog
x, xx: nat
rrest: list nat
Ih1: forall (p : prog) (input2 output : list nat), Forward (xx :: rrest) output = Some p -> Forward input2 nil = Some p' -> Forward ((xx :: rrest) ++ input2) output = Some (p ++ p')
Ih2: forall (p : prog) (input2 output : list nat), Forward rrest output = Some p -> Forward input2 nil = Some p' -> Forward (rrest ++ input2) output = Some (p ++ p')
p: prog
input2: list nat
y: nat
r: list nat
vrest: prog
eqnrest: Forward (xx :: rrest) r = Some vrest
xeqy: (x =? y) = true
v2: Forward input2 nil = Some p'match r with | nil => match rrest ++ input2 with | nil => None | _ :: rrest => match Forward rrest nil with | Some pp => Some (Select xx :: Backspace :: pp) | None => None end end | y :: r0 => if xx =? y then match Forward (rrest ++ input2) r0 with | Some pp => Some (Select xx :: pp) | None => None end else match rrest ++ input2 with | nil => None | _ :: rrest => match Forward rrest r with | Some pp => Some (Select xx :: Backspace :: pp) | None => None end end end = Some (vrest ++ p') -> match match r with | nil => match rrest ++ input2 with | nil => None | _ :: rrest => match Forward rrest nil with | Some pp => Some (Select xx :: Backspace :: pp) | None => None end end | y :: r0 => if xx =? y then match Forward (rrest ++ input2) r0 with | Some pp => Some (Select xx :: pp) | None => None end else match rrest ++ input2 with | nil => None | _ :: rrest => match Forward rrest r with | Some pp => Some (Select xx :: Backspace :: pp) | None => None end end end with | Some pp => Some (Select x :: pp) | None => None end = Some (Select x :: vrest ++ p')p': prog
x, xx: nat
rrest: list nat
Ih1: forall (p : prog) (input2 output : list nat), Forward (xx :: rrest) output = Some p -> Forward input2 nil = Some p' -> Forward ((xx :: rrest) ++ input2) output = Some (p ++ p')
Ih2: forall (p : prog) (input2 output : list nat), Forward rrest output = Some p -> Forward input2 nil = Some p' -> Forward (rrest ++ input2) output = Some (p ++ p')
p: prog
input2: list nat
y: nat
r: list nat
vrest: prog
eqnrest: Forward (xx :: rrest) r = Some vrest
xeqy: (x =? y) = true
v2: Forward input2 nil = Some p'
it: match r with | nil => match rrest ++ input2 with | nil => None | _ :: rrest => match Forward rrest nil with | Some pp => Some (Select xx :: Backspace :: pp) | None => None end end | y :: r0 => if xx =? y then match Forward (rrest ++ input2) r0 with | Some pp => Some (Select xx :: pp) | None => None end else match rrest ++ input2 with | nil => None | _ :: rrest => match Forward rrest r with | Some pp => Some (Select xx :: Backspace :: pp) | None => None end end end = Some (vrest ++ p')match match r with | nil => match rrest ++ input2 with | nil => None | _ :: rrest => match Forward rrest nil with | Some pp => Some (Select xx :: Backspace :: pp) | None => None end end | y :: r0 => if xx =? y then match Forward (rrest ++ input2) r0 with | Some pp => Some (Select xx :: pp) | None => None end else match rrest ++ input2 with | nil => None | _ :: rrest => match Forward rrest r with | Some pp => Some (Select xx :: Backspace :: pp) | None => None end end end with | Some pp => Some (Select x :: pp) | None => None end = Some (Select x :: vrest ++ p')easy.p': prog
x, xx: nat
rrest: list nat
Ih1: forall (p : prog) (input2 output : list nat), Forward (xx :: rrest) output = Some p -> Forward input2 nil = Some p' -> Forward ((xx :: rrest) ++ input2) output = Some (p ++ p')
Ih2: forall (p : prog) (input2 output : list nat), Forward rrest output = Some p -> Forward input2 nil = Some p' -> Forward (rrest ++ input2) output = Some (p ++ p')
p: prog
input2: list nat
y: nat
r: list nat
vrest: prog
eqnrest: Forward (xx :: rrest) r = Some vrest
xeqy: (x =? y) = true
v2: Forward input2 nil = Some p'
it: match r with | nil => match rrest ++ input2 with | nil => None | _ :: rrest => match Forward rrest nil with | Some pp => Some (Select xx :: Backspace :: pp) | None => None end end | y :: r0 => if xx =? y then match Forward (rrest ++ input2) r0 with | Some pp => Some (Select xx :: pp) | None => None end else match rrest ++ input2 with | nil => None | _ :: rrest => match Forward rrest r with | Some pp => Some (Select xx :: Backspace :: pp) | None => None end end end = Some (vrest ++ p')Some (Select x :: vrest ++ p') = Some (Select x :: vrest ++ p')p': prog
x, xx: nat
rrest: list nat
Ih1: forall (p : prog) (input2 output : list nat), Forward (xx :: rrest) output = Some p -> Forward input2 nil = Some p' -> Forward ((xx :: rrest) ++ input2) output = Some (p ++ p')
Ih2: forall (p : prog) (input2 output : list nat), Forward rrest output = Some p -> Forward input2 nil = Some p' -> Forward (rrest ++ input2) output = Some (p ++ p')
p: prog
input2: list nat
y: nat
r: list nat
vrest: prog
eqnrest: Forward (xx :: rrest) r = Some vrest
xeqy: (x =? y) = falsematch Forward rrest (y :: r) with | Some pp => Some (Select x :: Backspace :: pp) | None => None end = Some p -> Forward input2 nil = Some p' -> Forward ((x :: xx :: rrest) ++ input2) (y :: r) = Some (p ++ p')p': prog
x, xx: nat
rrest: list nat
Ih1: forall (p : prog) (input2 output : list nat), Forward (xx :: rrest) output = Some p -> Forward input2 nil = Some p' -> Forward ((xx :: rrest) ++ input2) output = Some (p ++ p')
Ih2: forall (p : prog) (input2 output : list nat), Forward rrest output = Some p -> Forward input2 nil = Some p' -> Forward (rrest ++ input2) output = Some (p ++ p')
p: prog
input2: list nat
y: nat
r: list nat
vrest: prog
eqnrest: Forward (xx :: rrest) r = Some vrest
xeqy: (x =? y) = false
v: prog
eqnrrest: Forward rrest (y :: r) = Some vSome (Select x :: Backspace :: v) = Some p -> Forward input2 nil = Some p' -> Forward ((x :: xx :: rrest) ++ input2) (y :: r) = Some (p ++ p')p': prog
x, xx: nat
rrest: list nat
Ih1: forall (p : prog) (input2 output : list nat), Forward (xx :: rrest) output = Some p -> Forward input2 nil = Some p' -> Forward ((xx :: rrest) ++ input2) output = Some (p ++ p')
Ih2: forall (p : prog) (input2 output : list nat), Forward rrest output = Some p -> Forward input2 nil = Some p' -> Forward (rrest ++ input2) output = Some (p ++ p')
p: prog
input2: list nat
y: nat
r: list nat
vrest: prog
eqnrest: Forward (xx :: rrest) r = Some vrest
xeqy: (x =? y) = false
v: prog
eqnrrest: Forward rrest (y :: r) = Some v
vp: Select x :: Backspace :: v = p
v2: Forward input2 nil = Some p'Forward ((x :: xx :: rrest) ++ input2) (y :: r) = Some (p ++ p')p': prog
x, xx: nat
rrest: list nat
Ih1: forall (p : prog) (input2 output : list nat), Forward (xx :: rrest) output = Some p -> Forward input2 nil = Some p' -> Forward ((xx :: rrest) ++ input2) output = Some (p ++ p')
Ih2: forall (p : prog) (input2 output : list nat), Forward rrest output = Some p -> Forward input2 nil = Some p' -> Forward (rrest ++ input2) output = Some (p ++ p')
p: prog
input2: list nat
y: nat
r: list nat
vrest: prog
eqnrest: Forward (xx :: rrest) r = Some vrest
xeqy: (x =? y) = false
v: prog
eqnrrest: Forward rrest (y :: r) = Some v
vp: Select x :: Backspace :: v = p
v2: Forward input2 nil = Some p'Forward ((x :: xx :: rrest) ++ input2) (y :: r) = Some ((Select x :: Backspace :: v) ++ p')p': prog
x, xx: nat
rrest: list nat
Ih1: forall (p : prog) (input2 output : list nat), Forward (xx :: rrest) output = Some p -> Forward input2 nil = Some p' -> Forward ((xx :: rrest) ++ input2) output = Some (p ++ p')
Ih2: forall (p : prog) (input2 output : list nat), Forward rrest output = Some p -> Forward input2 nil = Some p' -> Forward (rrest ++ input2) output = Some (p ++ p')
p: prog
input2: list nat
y: nat
r: list nat
vrest: prog
eqnrest: Forward (xx :: rrest) r = Some vrest
xeqy: (x =? y) = false
v: prog
eqnrrest: Forward rrest (y :: r) = Some v
v2: Forward input2 nil = Some p'Forward ((x :: xx :: rrest) ++ input2) (y :: r) = Some ((Select x :: Backspace :: v) ++ p')p': prog
x, xx: nat
rrest: list nat
Ih1: forall (p : prog) (input2 output : list nat), Forward (xx :: rrest) output = Some p -> Forward input2 nil = Some p' -> Forward ((xx :: rrest) ++ input2) output = Some (p ++ p')
Ih2: forall (p : prog) (input2 output : list nat), Forward rrest output = Some p -> Forward input2 nil = Some p' -> Forward (rrest ++ input2) output = Some (p ++ p')
p: prog
input2: list nat
y: nat
r: list nat
vrest: prog
eqnrest: Forward (xx :: rrest) r = Some vrest
xeqy: (x =? y) = false
v: prog
eqnrrest: Forward rrest (y :: r) = Some v
v2: Forward input2 nil = Some p'(if x =? y then match match r with | nil => match rrest ++ input2 with | nil => None | _ :: rrest => match Forward rrest nil with | Some pp => Some (Select xx :: Backspace :: pp) | None => None end end | y :: r0 => if xx =? y then match Forward (rrest ++ input2) r0 with | Some pp => Some (Select xx :: pp) | None => None end else match rrest ++ input2 with | nil => None | _ :: rrest => match Forward rrest r with | Some pp => Some (Select xx :: Backspace :: pp) | None => None end end end with | Some pp => Some (Select x :: pp) | None => None end else match Forward (rrest ++ input2) (y :: r) with | Some pp => Some (Select x :: Backspace :: pp) | None => None end) = Some (Select x :: Backspace :: v ++ p')easy.p': prog
x, xx: nat
rrest: list nat
Ih1: forall (p : prog) (input2 output : list nat), Forward (xx :: rrest) output = Some p -> Forward input2 nil = Some p' -> Forward ((xx :: rrest) ++ input2) output = Some (p ++ p')
Ih2: forall (p : prog) (input2 output : list nat), Forward rrest output = Some p -> Forward input2 nil = Some p' -> Forward (rrest ++ input2) output = Some (p ++ p')
p: prog
input2: list nat
y: nat
r: list nat
vrest: prog
eqnrest: Forward (xx :: rrest) r = Some vrest
xeqy: (x =? y) = false
v: prog
eqnrrest: Forward rrest (y :: r) = Some v
v2: Forward input2 nil = Some p'Some (Select x :: Backspace :: v ++ p') = Some (Select x :: Backspace :: v ++ p')p': prog
x, xx: nat
rrest: list nat
Ih1: forall (p : prog) (input2 output : list nat), Forward (xx :: rrest) output = Some p -> Forward input2 nil = Some p' -> Forward ((xx :: rrest) ++ input2) output = Some (p ++ p')
Ih2: forall (p : prog) (input2 output : list nat), Forward rrest output = Some p -> Forward input2 nil = Some p' -> Forward (rrest ++ input2) output = Some (p ++ p')
p: prog
input2: list nat
y: nat
r: list nat
eqnrest: Forward (xx :: rrest) r = None(if x =? y then None else match Forward rrest (y :: r) with | Some pp => Some (Select x :: Backspace :: pp) | None => None end) = Some p -> Forward input2 nil = Some p' -> Forward ((x :: xx :: rrest) ++ input2) (y :: r) = Some (p ++ p')p': prog
x, xx: nat
rrest: list nat
Ih1: forall (p : prog) (input2 output : list nat), Forward (xx :: rrest) output = Some p -> Forward input2 nil = Some p' -> Forward ((xx :: rrest) ++ input2) output = Some (p ++ p')
Ih2: forall (p : prog) (input2 output : list nat), Forward rrest output = Some p -> Forward input2 nil = Some p' -> Forward (rrest ++ input2) output = Some (p ++ p')
p: prog
input2: list nat
y: nat
r: list nat
eqnrest: Forward (xx :: rrest) r = None
xeqy: (x =? y) = falsematch Forward rrest (y :: r) with | Some pp => Some (Select x :: Backspace :: pp) | None => None end = Some p -> Forward input2 nil = Some p' -> Forward ((x :: xx :: rrest) ++ input2) (y :: r) = Some (p ++ p')p': prog
x, xx: nat
rrest: list nat
Ih1: forall (p : prog) (input2 output : list nat), Forward (xx :: rrest) output = Some p -> Forward input2 nil = Some p' -> Forward ((xx :: rrest) ++ input2) output = Some (p ++ p')
Ih2: forall (p : prog) (input2 output : list nat), Forward rrest output = Some p -> Forward input2 nil = Some p' -> Forward (rrest ++ input2) output = Some (p ++ p')
p: prog
input2: list nat
y: nat
r: list nat
eqnrest: Forward (xx :: rrest) r = None
xeqy: (x =? y) = false
v: prog
eqnrrest: Forward rrest (y :: r) = Some vSome (Select x :: Backspace :: v) = Some p -> Forward input2 nil = Some p' -> Forward ((x :: xx :: rrest) ++ input2) (y :: r) = Some (p ++ p')p': prog
x, xx: nat
rrest: list nat
Ih1: forall (p : prog) (input2 output : list nat), Forward (xx :: rrest) output = Some p -> Forward input2 nil = Some p' -> Forward ((xx :: rrest) ++ input2) output = Some (p ++ p')
Ih2: forall (p : prog) (input2 output : list nat), Forward rrest output = Some p -> Forward input2 nil = Some p' -> Forward (rrest ++ input2) output = Some (p ++ p')
p: prog
input2: list nat
y: nat
r: list nat
eqnrest: Forward (xx :: rrest) r = None
xeqy: (x =? y) = false
v: prog
eqnrrest: Forward rrest (y :: r) = Some v
vp: Select x :: Backspace :: v = p
v2: Forward input2 nil = Some p'Forward ((x :: xx :: rrest) ++ input2) (y :: r) = Some (p ++ p')p': prog
x, xx: nat
rrest: list nat
Ih1: forall (p : prog) (input2 output : list nat), Forward (xx :: rrest) output = Some p -> Forward input2 nil = Some p' -> Forward ((xx :: rrest) ++ input2) output = Some (p ++ p')
Ih2: forall (p : prog) (input2 output : list nat), Forward rrest output = Some p -> Forward input2 nil = Some p' -> Forward (rrest ++ input2) output = Some (p ++ p')
p: prog
input2: list nat
y: nat
r: list nat
eqnrest: Forward (xx :: rrest) r = None
xeqy: (x =? y) = false
v: prog
eqnrrest: Forward rrest (y :: r) = Some v
vp: Select x :: Backspace :: v = p
v2: Forward input2 nil = Some p'Forward ((x :: xx :: rrest) ++ input2) (y :: r) = Some ((Select x :: Backspace :: v) ++ p')p': prog
x, xx: nat
rrest: list nat
Ih1: forall (p : prog) (input2 output : list nat), Forward (xx :: rrest) output = Some p -> Forward input2 nil = Some p' -> Forward ((xx :: rrest) ++ input2) output = Some (p ++ p')
Ih2: forall (p : prog) (input2 output : list nat), Forward rrest output = Some p -> Forward input2 nil = Some p' -> Forward (rrest ++ input2) output = Some (p ++ p')
p: prog
input2: list nat
y: nat
r: list nat
eqnrest: Forward (xx :: rrest) r = None
xeqy: (x =? y) = false
v: prog
eqnrrest: Forward rrest (y :: r) = Some v
v2: Forward input2 nil = Some p'Forward ((x :: xx :: rrest) ++ input2) (y :: r) = Some ((Select x :: Backspace :: v) ++ p')p': prog
x, xx: nat
rrest: list nat
Ih1: forall (p : prog) (input2 output : list nat), Forward (xx :: rrest) output = Some p -> Forward input2 nil = Some p' -> Forward ((xx :: rrest) ++ input2) output = Some (p ++ p')
Ih2: forall (p : prog) (input2 output : list nat), Forward rrest output = Some p -> Forward input2 nil = Some p' -> Forward (rrest ++ input2) output = Some (p ++ p')
p: prog
input2: list nat
y: nat
r: list nat
eqnrest: Forward (xx :: rrest) r = None
xeqy: (x =? y) = false
v: prog
eqnrrest: Forward rrest (y :: r) = Some v
v2: Forward input2 nil = Some p'(if x =? y then match match r with | nil => match rrest ++ input2 with | nil => None | _ :: rrest => match Forward rrest nil with | Some pp => Some (Select xx :: Backspace :: pp) | None => None end end | y :: r0 => if xx =? y then match Forward (rrest ++ input2) r0 with | Some pp => Some (Select xx :: pp) | None => None end else match rrest ++ input2 with | nil => None | _ :: rrest => match Forward rrest r with | Some pp => Some (Select xx :: Backspace :: pp) | None => None end end end with | Some pp => Some (Select x :: pp) | None => None end else match Forward (rrest ++ input2) (y :: r) with | Some pp => Some (Select x :: Backspace :: pp) | None => None end) = Some (Select x :: Backspace :: v ++ p')easy. Qed.p': prog
x, xx: nat
rrest: list nat
Ih1: forall (p : prog) (input2 output : list nat), Forward (xx :: rrest) output = Some p -> Forward input2 nil = Some p' -> Forward ((xx :: rrest) ++ input2) output = Some (p ++ p')
Ih2: forall (p : prog) (input2 output : list nat), Forward rrest output = Some p -> Forward input2 nil = Some p' -> Forward (rrest ++ input2) output = Some (p ++ p')
p: prog
input2: list nat
y: nat
r: list nat
eqnrest: Forward (xx :: rrest) r = None
xeqy: (x =? y) = false
v: prog
eqnrrest: Forward rrest (y :: r) = Some v
v2: Forward input2 nil = Some p'Some (Select x :: Backspace :: v ++ p') = Some (Select x :: Backspace :: v ++ p')A few comments on this solution:
The code posted in the original function contains 3 recursive calls, one where the argument is the immediate sublist (rest) and 2 where the argument is the second sublist (rest). The first one is handled by induction hypothesis Ih1 and the other are handled by induction hypothesis Ih2. For a reason I have no time to investigate, my proof needs 4 uses of induction hypotheses instead of 3. This means that there is probably some duplication.
Sometimes, the simpl tactic is too eager to unroll the recursive definition until it can no longer do anything. To counterbalance this bias of the simpl tactic, I had to perform one of the unrolling steps by hand, without relying on simpl. This unrolling step is performed by the change tactic call that appears in the middle of the script.
Everytime that there is a recursive call in your function, the result is later analyzed by a match construct. To account for this, the proof perform case analysis on the results of recursive calls and uses the destruct ... eqn:... variant of the destruct tactic to perform this analysis.
Aside from these advanced techniques, the proof is just guided by the interaction with Coq.
This proof script was verified with coq-8.15 with the List and ZArith modules imported.
You can avoid constructing a tailored induction principle by relying on much more powerful well founded induction. This will give you a more general induction hypothesis, which can be used for a much wider set of recursive arguments (even arguments that are not structural subterms of the initial first list). Here is the full script:
Require Import Wellfounded.
forall (p p' : prog) (input1 input2 output : list nat), Forward input1 output = Some p -> Forward input2 nil = Some p' -> Forward (input1 ++ input2) output = Some (p ++ p')forall (p p' : prog) (input1 input2 output : list nat), Forward input1 output = Some p -> Forward input2 nil = Some p' -> Forward (input1 ++ input2) output = Some (p ++ p')p, p': prog
input1: list natforall input2 output : list nat, Forward input1 output = Some p -> Forward input2 nil = Some p' -> Forward (input1 ++ input2) output = Some (p ++ p')p': prog
input1: list natforall (p : prog) (input2 output : list nat), Forward input1 output = Some p -> Forward input2 nil = Some p' -> Forward (input1 ++ input2) output = Some (p ++ p')p': prog
input1: list nat
Ih: forall y : list nat, length y < length input1 -> forall (p : prog) (input2 output : list nat), Forward y output = Some p -> Forward input2 nil = Some p' -> Forward (y ++ input2) output = Some (p ++ p')forall (p : prog) (input2 output : list nat), Forward input1 output = Some p -> Forward input2 nil = Some p' -> Forward (input1 ++ input2) output = Some (p ++ p')p': prog
input1: list nat
input1eq: input1 = nil
Ih: forall y : list nat, length y < length nil -> forall (p : prog) (input2 output : list nat), Forward y output = Some p -> Forward input2 nil = Some p' -> Forward (y ++ input2) output = Some (p ++ p')forall (p : prog) (input2 output : list nat), Forward nil output = Some p -> Forward input2 nil = Some p' -> Forward (nil ++ input2) output = Some (p ++ p')p': prog
input1: list nat
x: nat
input1eq: input1 = x :: nil
Ih: forall y : list nat, length y < length (x :: nil) -> forall (p : prog) (input2 output : list nat), Forward y output = Some p -> Forward input2 nil = Some p' -> Forward (y ++ input2) output = Some (p ++ p')forall (p : prog) (input2 output : list nat), Forward (x :: nil) output = Some p -> Forward input2 nil = Some p' -> Forward ((x :: nil) ++ input2) output = Some (p ++ p')p': prog
input1: list nat
x, xx: nat
rrest: list nat
input1eq: input1 = x :: xx :: rrest
Ih: forall y : list nat, length y < length (x :: xx :: rrest) -> forall (p : prog) (input2 output : list nat), Forward y output = Some p -> Forward input2 nil = Some p' -> Forward (y ++ input2) output = Some (p ++ p')forall (p : prog) (input2 output : list nat), Forward (x :: xx :: rrest) output = Some p -> Forward input2 nil = Some p' -> Forward ((x :: xx :: rrest) ++ input2) output = Some (p ++ p')p': prog
input1: list nat
input1eq: input1 = nil
Ih: forall y : list nat, length y < length nil -> forall (p : prog) (input2 output : list nat), Forward y output = Some p -> Forward input2 nil = Some p' -> Forward (y ++ input2) output = Some (p ++ p')forall (p : prog) (input2 output : list nat), Forward nil output = Some p -> Forward input2 nil = Some p' -> Forward (nil ++ input2) output = Some (p ++ p')p': prog
input1: list nat
input1eq: input1 = nil
Ih: forall y : list nat, length y < length nil -> forall (p : prog) (input2 output : list nat), Forward y output = Some p -> Forward input2 nil = Some p' -> Forward (y ++ input2) output = Some (p ++ p')
p: prog
input2: list natForward nil nil = Some p -> Forward input2 nil = Some p' -> Forward (nil ++ input2) nil = Some (p ++ p')p': prog
input1: list nat
input1eq: input1 = nil
Ih: forall y : list nat, length y < length nil -> forall (p : prog) (input2 output : list nat), Forward y output = Some p -> Forward input2 nil = Some p' -> Forward (y ++ input2) output = Some (p ++ p')
p: prog
input2: list nat
no1: nat
output: list natForward nil (no1 :: output) = Some p -> Forward input2 nil = Some p' -> Forward (nil ++ input2) (no1 :: output) = Some (p ++ p')p': prog
input1: list nat
input1eq: input1 = nil
Ih: forall y : list nat, length y < length nil -> forall (p : prog) (input2 output : list nat), Forward y output = Some p -> Forward input2 nil = Some p' -> Forward (y ++ input2) output = Some (p ++ p')
p: prog
input2: list natForward nil nil = Some p -> Forward input2 nil = Some p' -> Forward (nil ++ input2) nil = Some (p ++ p')p': prog
input1: list nat
input1eq: input1 = nil
Ih: forall y : list nat, length y < length nil -> forall (p : prog) (input2 output : list nat), Forward y output = Some p -> Forward input2 nil = Some p' -> Forward (y ++ input2) output = Some (p ++ p')
p: prog
input2: list nat
p_is_nil: nil = pForward input2 nil = Some p' -> Forward (nil ++ input2) nil = Some (p ++ p')p': prog
input1: list nat
input1eq: input1 = nil
Ih: forall y : list nat, length y < length nil -> forall (p : prog) (input2 output : list nat), Forward y output = Some p -> Forward input2 nil = Some p' -> Forward (y ++ input2) output = Some (p ++ p')
p: prog
input2: list nat
p_is_nil: nil = pForward input2 nil = Some p' -> Forward (nil ++ input2) nil = Some (nil ++ p')auto.p': prog
input1: list nat
input1eq: input1 = nil
Ih: forall y : list nat, length y < length nil -> forall (p : prog) (input2 output : list nat), Forward y output = Some p -> Forward input2 nil = Some p' -> Forward (y ++ input2) output = Some (p ++ p')
p: prog
input2: list nat
p_is_nil: nil = pForward input2 nil = Some p' -> Forward input2 nil = Some p'discriminate.p': prog
input1: list nat
input1eq: input1 = nil
Ih: forall y : list nat, length y < length nil -> forall (p : prog) (input2 output : list nat), Forward y output = Some p -> Forward input2 nil = Some p' -> Forward (y ++ input2) output = Some (p ++ p')
p: prog
input2: list nat
no1: nat
output: list natForward nil (no1 :: output) = Some p -> Forward input2 nil = Some p' -> Forward (nil ++ input2) (no1 :: output) = Some (p ++ p')p': prog
input1: list nat
x: nat
input1eq: input1 = x :: nil
Ih: forall y : list nat, length y < length (x :: nil) -> forall (p : prog) (input2 output : list nat), Forward y output = Some p -> Forward input2 nil = Some p' -> Forward (y ++ input2) output = Some (p ++ p')forall (p : prog) (input2 output : list nat), Forward (x :: nil) output = Some p -> Forward input2 nil = Some p' -> Forward ((x :: nil) ++ input2) output = Some (p ++ p')p': prog
input1: list nat
x: nat
input1eq: input1 = x :: nil
Ih: forall y : list nat, length y < length (x :: nil) -> forall (p : prog) (input2 output : list nat), Forward y output = Some p -> Forward input2 nil = Some p' -> Forward (y ++ input2) output = Some (p ++ p')forall (p : prog) (input2 output : list nat), match output with | nil => None | y :: r => if x =? y then match match r with | nil => Some nil | _ :: _ => None end with | Some pp => Some (Select x :: pp) | None => None end else None end = Some p -> Forward input2 nil = Some p' -> match output with | nil => match input2 with | nil => None | _ :: rrest => match Forward rrest nil with | Some pp => Some (Select x :: Backspace :: pp) | None => None end end | y :: r => if x =? y then match Forward input2 r with | Some pp => Some (Select x :: pp) | None => None end else match input2 with | nil => None | _ :: rrest => match Forward rrest output with | Some pp => Some (Select x :: Backspace :: pp) | None => None end end end = Some (p ++ p')p': prog
input1: list nat
x: nat
input1eq: input1 = x :: nil
Ih: forall y : list nat, length y < length (x :: nil) -> forall (p : prog) (input2 output : list nat), Forward y output = Some p -> Forward input2 nil = Some p' -> Forward (y ++ input2) output = Some (p ++ p')
p: prog
input2: list nat
y: nat
r: list nat(if x =? y then match match r with | nil => Some nil | _ :: _ => None end with | Some pp => Some (Select x :: pp) | None => None end else None) = Some p -> Forward input2 nil = Some p' -> (if x =? y then match Forward input2 r with | Some pp => Some (Select x :: pp) | None => None end else match input2 with | nil => None | _ :: rrest => match Forward rrest (y :: r) with | Some pp => Some (Select x :: Backspace :: pp) | None => None end end) = Some (p ++ p')p': prog
input1: list nat
x: nat
input1eq: input1 = x :: nil
Ih: forall y : list nat, length y < length (x :: nil) -> forall (p : prog) (input2 output : list nat), Forward y output = Some p -> Forward input2 nil = Some p' -> Forward (y ++ input2) output = Some (p ++ p')
p: prog
input2: list nat
y: nat
r: list natmatch match r with | nil => Some nil | _ :: _ => None end with | Some pp => Some (Select x :: pp) | None => None end = Some p -> Forward input2 nil = Some p' -> match Forward input2 r with | Some pp => Some (Select x :: pp) | None => None end = Some (p ++ p')now intros [= pval] v2; rewrite <- pval, v2; simpl.p': prog
input1: list nat
x: nat
input1eq: input1 = x :: nil
Ih: forall y : list nat, length y < length (x :: nil) -> forall (p : prog) (input2 output : list nat), Forward y output = Some p -> Forward input2 nil = Some p' -> Forward (y ++ input2) output = Some (p ++ p')
p: prog
input2: list nat
y: natSome (Select x :: nil) = Some p -> Forward input2 nil = Some p' -> match Forward input2 nil with | Some pp => Some (Select x :: pp) | None => None end = Some (p ++ p')p': prog
input1: list nat
x, xx: nat
rrest: list nat
input1eq: input1 = x :: xx :: rrest
Ih: forall y : list nat, length y < length (x :: xx :: rrest) -> forall (p : prog) (input2 output : list nat), Forward y output = Some p -> Forward input2 nil = Some p' -> Forward (y ++ input2) output = Some (p ++ p')forall (p : prog) (input2 output : list nat), Forward (x :: xx :: rrest) output = Some p -> Forward input2 nil = Some p' -> Forward ((x :: xx :: rrest) ++ input2) output = Some (p ++ p')p': prog
input1: list nat
x, xx: nat
rrest: list nat
input1eq: input1 = x :: xx :: rrest
Ih: forall y : list nat, length y < length (x :: xx :: rrest) -> forall (p : prog) (input2 output : list nat), Forward y output = Some p -> Forward input2 nil = Some p' -> Forward (y ++ input2) output = Some (p ++ p')
p: prog
input2, output: list natForward (x :: xx :: rrest) output = Some p -> Forward input2 nil = Some p' -> Forward ((x :: xx :: rrest) ++ input2) output = Some (p ++ p')p': prog
input1: list nat
x, xx: nat
rrest: list nat
input1eq: input1 = x :: xx :: rrest
Ih: forall y : list nat, length y < length (x :: xx :: rrest) -> forall (p : prog) (input2 output : list nat), Forward y output = Some p -> Forward input2 nil = Some p' -> Forward (y ++ input2) output = Some (p ++ p')
p: prog
input2, output: list natlength rrest < length (x :: xx :: rrest)p': prog
input1: list nat
x, xx: nat
rrest: list nat
input1eq: input1 = x :: xx :: rrest
Ih: forall y : list nat, length y < length (x :: xx :: rrest) -> forall (p : prog) (input2 output : list nat), Forward y output = Some p -> Forward input2 nil = Some p' -> Forward (y ++ input2) output = Some (p ++ p')
p: prog
input2, output: list nat
rrestlt: length rrest < length (x :: xx :: rrest)Forward (x :: xx :: rrest) output = Some p -> Forward input2 nil = Some p' -> Forward ((x :: xx :: rrest) ++ input2) output = Some (p ++ p')now simpl; auto with arith.p': prog
input1: list nat
x, xx: nat
rrest: list nat
input1eq: input1 = x :: xx :: rrest
Ih: forall y : list nat, length y < length (x :: xx :: rrest) -> forall (p : prog) (input2 output : list nat), Forward y output = Some p -> Forward input2 nil = Some p' -> Forward (y ++ input2) output = Some (p ++ p')
p: prog
input2, output: list natlength rrest < length (x :: xx :: rrest)p': prog
input1: list nat
x, xx: nat
rrest: list nat
input1eq: input1 = x :: xx :: rrest
Ih: forall y : list nat, length y < length (x :: xx :: rrest) -> forall (p : prog) (input2 output : list nat), Forward y output = Some p -> Forward input2 nil = Some p' -> Forward (y ++ input2) output = Some (p ++ p')
p: prog
input2, output: list nat
rrestlt: length rrest < length (x :: xx :: rrest)Forward (x :: xx :: rrest) output = Some p -> Forward input2 nil = Some p' -> Forward ((x :: xx :: rrest) ++ input2) output = Some (p ++ p')p': prog
input1: list nat
x, xx: nat
rrest: list nat
input1eq: input1 = x :: xx :: rrest
Ih: forall y : list nat, length y < length (x :: xx :: rrest) -> forall (p : prog) (input2 output : list nat), Forward y output = Some p -> Forward input2 nil = Some p' -> Forward (y ++ input2) output = Some (p ++ p')
p: prog
input2, output: list nat
rrestlt: length rrest < length (x :: xx :: rrest)length (xx :: rrest) < length (x :: xx :: rrest)p': prog
input1: list nat
x, xx: nat
rrest: list nat
input1eq: input1 = x :: xx :: rrest
Ih: forall y : list nat, length y < length (x :: xx :: rrest) -> forall (p : prog) (input2 output : list nat), Forward y output = Some p -> Forward input2 nil = Some p' -> Forward (y ++ input2) output = Some (p ++ p')
p: prog
input2, output: list nat
rrestlt: length rrest < length (x :: xx :: rrest)
restlt: length (xx :: rrest) < length (x :: xx :: rrest)Forward (x :: xx :: rrest) output = Some p -> Forward input2 nil = Some p' -> Forward ((x :: xx :: rrest) ++ input2) output = Some (p ++ p')now simpl; auto with arith.p': prog
input1: list nat
x, xx: nat
rrest: list nat
input1eq: input1 = x :: xx :: rrest
Ih: forall y : list nat, length y < length (x :: xx :: rrest) -> forall (p : prog) (input2 output : list nat), Forward y output = Some p -> Forward input2 nil = Some p' -> Forward (y ++ input2) output = Some (p ++ p')
p: prog
input2, output: list nat
rrestlt: length rrest < length (x :: xx :: rrest)length (xx :: rrest) < length (x :: xx :: rrest)p': prog
input1: list nat
x, xx: nat
rrest: list nat
input1eq: input1 = x :: xx :: rrest
Ih: forall y : list nat, length y < length (x :: xx :: rrest) -> forall (p : prog) (input2 output : list nat), Forward y output = Some p -> Forward input2 nil = Some p' -> Forward (y ++ input2) output = Some (p ++ p')
p: prog
input2, output: list nat
rrestlt: length rrest < length (x :: xx :: rrest)
restlt: length (xx :: rrest) < length (x :: xx :: rrest)Forward (x :: xx :: rrest) output = Some p -> Forward input2 nil = Some p' -> Forward ((x :: xx :: rrest) ++ input2) output = Some (p ++ p')p': prog
input1: list nat
x, xx: nat
rrest: list nat
input1eq: input1 = x :: xx :: rrest
Ih: forall y : list nat, length y < length (x :: xx :: rrest) -> forall (p : prog) (input2 output : list nat), Forward y output = Some p -> Forward input2 nil = Some p' -> Forward (y ++ input2) output = Some (p ++ p')
p: prog
input2: list nat
rrestlt: length rrest < length (x :: xx :: rrest)
restlt: length (xx :: rrest) < length (x :: xx :: rrest)Forward (x :: xx :: rrest) nil = Some p -> Forward input2 nil = Some p' -> Forward ((x :: xx :: rrest) ++ input2) nil = Some (p ++ p')p': prog
input1: list nat
x, xx: nat
rrest: list nat
input1eq: input1 = x :: xx :: rrest
Ih: forall y : list nat, length y < length (x :: xx :: rrest) -> forall (p : prog) (input2 output : list nat), Forward y output = Some p -> Forward input2 nil = Some p' -> Forward (y ++ input2) output = Some (p ++ p')
p: prog
input2: list nat
y: nat
r: list nat
rrestlt: length rrest < length (x :: xx :: rrest)
restlt: length (xx :: rrest) < length (x :: xx :: rrest)Forward (x :: xx :: rrest) (y :: r) = Some p -> Forward input2 nil = Some p' -> Forward ((x :: xx :: rrest) ++ input2) (y :: r) = Some (p ++ p')p': prog
input1: list nat
x, xx: nat
rrest: list nat
input1eq: input1 = x :: xx :: rrest
Ih: forall y : list nat, length y < length (x :: xx :: rrest) -> forall (p : prog) (input2 output : list nat), Forward y output = Some p -> Forward input2 nil = Some p' -> Forward (y ++ input2) output = Some (p ++ p')
p: prog
input2: list nat
rrestlt: length rrest < length (x :: xx :: rrest)
restlt: length (xx :: rrest) < length (x :: xx :: rrest)Forward (x :: xx :: rrest) nil = Some p -> Forward input2 nil = Some p' -> Forward ((x :: xx :: rrest) ++ input2) nil = Some (p ++ p')p': prog
input1: list nat
x, xx: nat
rrest: list nat
input1eq: input1 = x :: xx :: rrest
Ih: forall y : list nat, length y < length (x :: xx :: rrest) -> forall (p : prog) (input2 output : list nat), Forward y output = Some p -> Forward input2 nil = Some p' -> Forward (y ++ input2) output = Some (p ++ p')
p: prog
input2: list nat
rrestlt: length rrest < length (x :: xx :: rrest)
restlt: length (xx :: rrest) < length (x :: xx :: rrest)match Forward rrest nil with | Some pp => Some (Select x :: Backspace :: pp) | None => None end = Some p -> Forward input2 nil = Some p' -> Forward ((x :: xx :: rrest) ++ input2) nil = Some (p ++ p')p': prog
input1: list nat
x, xx: nat
rrest: list nat
input1eq: input1 = x :: xx :: rrest
Ih: forall y : list nat, length y < length (x :: xx :: rrest) -> forall (p : prog) (input2 output : list nat), Forward y output = Some p -> Forward input2 nil = Some p' -> Forward (y ++ input2) output = Some (p ++ p')
p: prog
input2: list nat
rrestlt: length rrest < length (x :: xx :: rrest)
restlt: length (xx :: rrest) < length (x :: xx :: rrest)
v: prog
vtl: Forward rrest nil = Some vSome (Select x :: Backspace :: v) = Some p -> Forward input2 nil = Some p' -> Forward ((x :: xx :: rrest) ++ input2) nil = Some (p ++ p')p': prog
input1: list nat
x, xx: nat
rrest: list nat
input1eq: input1 = x :: xx :: rrest
Ih: forall y : list nat, length y < length (x :: xx :: rrest) -> forall (p : prog) (input2 output : list nat), Forward y output = Some p -> Forward input2 nil = Some p' -> Forward (y ++ input2) output = Some (p ++ p')
p: prog
input2: list nat
rrestlt: length rrest < length (x :: xx :: rrest)
restlt: length (xx :: rrest) < length (x :: xx :: rrest)
v: prog
vtl: Forward rrest nil = Some v
pval: Select x :: Backspace :: v = p
p'val: Forward input2 nil = Some p'Forward ((x :: xx :: rrest) ++ input2) nil = Some (p ++ p')p': prog
input1: list nat
x, xx: nat
rrest: list nat
input1eq: input1 = x :: xx :: rrest
Ih: forall y : list nat, length y < length (x :: xx :: rrest) -> forall (p : prog) (input2 output : list nat), Forward y output = Some p -> Forward input2 nil = Some p' -> Forward (y ++ input2) output = Some (p ++ p')
p: prog
input2: list nat
rrestlt: length rrest < length (x :: xx :: rrest)
restlt: length (xx :: rrest) < length (x :: xx :: rrest)
v: prog
vtl: Forward rrest nil = Some v
pval: Select x :: Backspace :: v = p
p'val: Forward input2 nil = Some p'
tmp: Forward (rrest ++ input2) nil = Some (v ++ p')Forward ((x :: xx :: rrest) ++ input2) nil = Some (p ++ p')p': prog
input1: list nat
x, xx: nat
rrest: list nat
input1eq: input1 = x :: xx :: rrest
Ih: forall y : list nat, length y < length (x :: xx :: rrest) -> forall (p : prog) (input2 output : list nat), Forward y output = Some p -> Forward input2 nil = Some p' -> Forward (y ++ input2) output = Some (p ++ p')
p: prog
input2: list nat
rrestlt: length rrest < length (x :: xx :: rrest)
restlt: length (xx :: rrest) < length (x :: xx :: rrest)
v: prog
vtl: Forward rrest nil = Some v
pval: Select x :: Backspace :: v = p
p'val: Forward input2 nil = Some p'
tmp: Forward (rrest ++ input2) nil = Some (v ++ p')match Forward (rrest ++ input2) nil with | Some pp => Some (Select x :: Backspace :: pp) | None => None end = Some (p ++ p')easy.p': prog
input1: list nat
x, xx: nat
rrest: list nat
input1eq: input1 = x :: xx :: rrest
Ih: forall y : list nat, length y < length (x :: xx :: rrest) -> forall (p : prog) (input2 output : list nat), Forward y output = Some p -> Forward input2 nil = Some p' -> Forward (y ++ input2) output = Some (p ++ p')
p: prog
input2: list nat
rrestlt: length rrest < length (x :: xx :: rrest)
restlt: length (xx :: rrest) < length (x :: xx :: rrest)
v: prog
vtl: Forward rrest nil = Some v
pval: Select x :: Backspace :: v = p
p'val: Forward input2 nil = Some p'
tmp: Forward (rrest ++ input2) nil = Some (v ++ p')Some (Select x :: Backspace :: v ++ p') = Some ((Select x :: Backspace :: v) ++ p')p': prog
input1: list nat
x, xx: nat
rrest: list nat
input1eq: input1 = x :: xx :: rrest
Ih: forall y : list nat, length y < length (x :: xx :: rrest) -> forall (p : prog) (input2 output : list nat), Forward y output = Some p -> Forward input2 nil = Some p' -> Forward (y ++ input2) output = Some (p ++ p')
p: prog
input2: list nat
y: nat
r: list nat
rrestlt: length rrest < length (x :: xx :: rrest)
restlt: length (xx :: rrest) < length (x :: xx :: rrest)Forward (x :: xx :: rrest) (y :: r) = Some p -> Forward input2 nil = Some p' -> Forward ((x :: xx :: rrest) ++ input2) (y :: r) = Some (p ++ p')p': prog
input1: list nat
x, xx: nat
rrest: list nat
input1eq: input1 = x :: xx :: rrest
Ih: forall y : list nat, length y < length (x :: xx :: rrest) -> forall (p : prog) (input2 output : list nat), Forward y output = Some p -> Forward input2 nil = Some p' -> Forward (y ++ input2) output = Some (p ++ p')
p: prog
input2: list nat
y: nat
r: list nat
rrestlt: length rrest < length (x :: xx :: rrest)
restlt: length (xx :: rrest) < length (x :: xx :: rrest)(if x =? y then match Forward (xx :: rrest) r with | Some pp => Some (Select x :: pp) | None => None end else match Forward rrest (y :: r) with | Some pp => Some (Select x :: Backspace :: pp) | None => None end) = Some p -> Forward input2 nil = Some p' -> Forward ((x :: xx :: rrest) ++ input2) (y :: r) = Some (p ++ p')p': prog
input1: list nat
x, xx: nat
rrest: list nat
input1eq: input1 = x :: xx :: rrest
Ih: forall y : list nat, length y < length (x :: xx :: rrest) -> forall (p : prog) (input2 output : list nat), Forward y output = Some p -> Forward input2 nil = Some p' -> Forward (y ++ input2) output = Some (p ++ p')
p: prog
input2: list nat
y: nat
r: list nat
rrestlt: length rrest < length (x :: xx :: rrest)
restlt: length (xx :: rrest) < length (x :: xx :: rrest)
vrest: prog
eqnrest: Forward (xx :: rrest) r = Some vrest(if x =? y then Some (Select x :: vrest) else match Forward rrest (y :: r) with | Some pp => Some (Select x :: Backspace :: pp) | None => None end) = Some p -> Forward input2 nil = Some p' -> Forward ((x :: xx :: rrest) ++ input2) (y :: r) = Some (p ++ p')p': prog
input1: list nat
x, xx: nat
rrest: list nat
input1eq: input1 = x :: xx :: rrest
Ih: forall y : list nat, length y < length (x :: xx :: rrest) -> forall (p : prog) (input2 output : list nat), Forward y output = Some p -> Forward input2 nil = Some p' -> Forward (y ++ input2) output = Some (p ++ p')
p: prog
input2: list nat
y: nat
r: list nat
rrestlt: length rrest < length (x :: xx :: rrest)
restlt: length (xx :: rrest) < length (x :: xx :: rrest)
eqnrest: Forward (xx :: rrest) r = None(if x =? y then None else match Forward rrest (y :: r) with | Some pp => Some (Select x :: Backspace :: pp) | None => None end) = Some p -> Forward input2 nil = Some p' -> Forward ((x :: xx :: rrest) ++ input2) (y :: r) = Some (p ++ p')p': prog
input1: list nat
x, xx: nat
rrest: list nat
input1eq: input1 = x :: xx :: rrest
Ih: forall y : list nat, length y < length (x :: xx :: rrest) -> forall (p : prog) (input2 output : list nat), Forward y output = Some p -> Forward input2 nil = Some p' -> Forward (y ++ input2) output = Some (p ++ p')
p: prog
input2: list nat
y: nat
r: list nat
rrestlt: length rrest < length (x :: xx :: rrest)
restlt: length (xx :: rrest) < length (x :: xx :: rrest)
vrest: prog
eqnrest: Forward (xx :: rrest) r = Some vrest(if x =? y then Some (Select x :: vrest) else match Forward rrest (y :: r) with | Some pp => Some (Select x :: Backspace :: pp) | None => None end) = Some p -> Forward input2 nil = Some p' -> Forward ((x :: xx :: rrest) ++ input2) (y :: r) = Some (p ++ p')p': prog
input1: list nat
x, xx: nat
rrest: list nat
input1eq: input1 = x :: xx :: rrest
Ih: forall y : list nat, length y < length (x :: xx :: rrest) -> forall (p : prog) (input2 output : list nat), Forward y output = Some p -> Forward input2 nil = Some p' -> Forward (y ++ input2) output = Some (p ++ p')
p: prog
input2: list nat
y: nat
r: list nat
rrestlt: length rrest < length (x :: xx :: rrest)
restlt: length (xx :: rrest) < length (x :: xx :: rrest)
vrest: prog
eqnrest: Forward (xx :: rrest) r = Some vrest
xeqy: (x =? y) = trueSome (Select x :: vrest) = Some p -> Forward input2 nil = Some p' -> Forward ((x :: xx :: rrest) ++ input2) (y :: r) = Some (p ++ p')p': prog
input1: list nat
x, xx: nat
rrest: list nat
input1eq: input1 = x :: xx :: rrest
Ih: forall y : list nat, length y < length (x :: xx :: rrest) -> forall (p : prog) (input2 output : list nat), Forward y output = Some p -> Forward input2 nil = Some p' -> Forward (y ++ input2) output = Some (p ++ p')
p: prog
input2: list nat
y: nat
r: list nat
rrestlt: length rrest < length (x :: xx :: rrest)
restlt: length (xx :: rrest) < length (x :: xx :: rrest)
vrest: prog
eqnrest: Forward (xx :: rrest) r = Some vrest
xeqy: (x =? y) = falsematch Forward rrest (y :: r) with | Some pp => Some (Select x :: Backspace :: pp) | None => None end = Some p -> Forward input2 nil = Some p' -> Forward ((x :: xx :: rrest) ++ input2) (y :: r) = Some (p ++ p')p': prog
input1: list nat
x, xx: nat
rrest: list nat
input1eq: input1 = x :: xx :: rrest
Ih: forall y : list nat, length y < length (x :: xx :: rrest) -> forall (p : prog) (input2 output : list nat), Forward y output = Some p -> Forward input2 nil = Some p' -> Forward (y ++ input2) output = Some (p ++ p')
p: prog
input2: list nat
y: nat
r: list nat
rrestlt: length rrest < length (x :: xx :: rrest)
restlt: length (xx :: rrest) < length (x :: xx :: rrest)
vrest: prog
eqnrest: Forward (xx :: rrest) r = Some vrest
xeqy: (x =? y) = trueSome (Select x :: vrest) = Some p -> Forward input2 nil = Some p' -> Forward ((x :: xx :: rrest) ++ input2) (y :: r) = Some (p ++ p')p': prog
input1: list nat
x, xx: nat
rrest: list nat
input1eq: input1 = x :: xx :: rrest
Ih: forall y : list nat, length y < length (x :: xx :: rrest) -> forall (p : prog) (input2 output : list nat), Forward y output = Some p -> Forward input2 nil = Some p' -> Forward (y ++ input2) output = Some (p ++ p')
p: prog
input2: list nat
y: nat
r: list nat
rrestlt: length rrest < length (x :: xx :: rrest)
restlt: length (xx :: rrest) < length (x :: xx :: rrest)
vrest: prog
eqnrest: Forward (xx :: rrest) r = Some vrest
xeqy: (x =? y) = true
vp: Select x :: vrest = p
v2: Forward input2 nil = Some p'Forward ((x :: xx :: rrest) ++ input2) (y :: r) = Some (p ++ p')p': prog
input1: list nat
x, xx: nat
rrest: list nat
input1eq: input1 = x :: xx :: rrest
Ih: forall y : list nat, length y < length (x :: xx :: rrest) -> forall (p : prog) (input2 output : list nat), Forward y output = Some p -> Forward input2 nil = Some p' -> Forward (y ++ input2) output = Some (p ++ p')
p: prog
input2: list nat
y: nat
r: list nat
rrestlt: length rrest < length (x :: xx :: rrest)
restlt: length (xx :: rrest) < length (x :: xx :: rrest)
vrest: prog
eqnrest: Forward (xx :: rrest) r = Some vrest
xeqy: (x =? y) = true
vp: Select x :: vrest = p
v2: Forward input2 nil = Some p'Forward ((x :: xx :: rrest) ++ input2) (y :: r) = Some ((Select x :: vrest) ++ p')p': prog
input1: list nat
x, xx: nat
rrest: list nat
input1eq: input1 = x :: xx :: rrest
Ih: forall y : list nat, length y < length (x :: xx :: rrest) -> forall (p : prog) (input2 output : list nat), Forward y output = Some p -> Forward input2 nil = Some p' -> Forward (y ++ input2) output = Some (p ++ p')
p: prog
input2: list nat
y: nat
r: list nat
rrestlt: length rrest < length (x :: xx :: rrest)
restlt: length (xx :: rrest) < length (x :: xx :: rrest)
vrest: prog
eqnrest: Forward (xx :: rrest) r = Some vrest
xeqy: (x =? y) = true
v2: Forward input2 nil = Some p'Forward ((x :: xx :: rrest) ++ input2) (y :: r) = Some ((Select x :: vrest) ++ p')p': prog
input1: list nat
x, xx: nat
rrest: list nat
input1eq: input1 = x :: xx :: rrest
Ih: forall y : list nat, length y < length (x :: xx :: rrest) -> forall (p : prog) (input2 output : list nat), Forward y output = Some p -> Forward input2 nil = Some p' -> Forward (y ++ input2) output = Some (p ++ p')
p: prog
input2: list nat
y: nat
r: list nat
rrestlt: length rrest < length (x :: xx :: rrest)
restlt: length (xx :: rrest) < length (x :: xx :: rrest)
vrest: prog
eqnrest: Forward (xx :: rrest) r = Some vrest
xeqy: (x =? y) = true
v2: Forward input2 nil = Some p'Forward ((xx :: rrest) ++ input2) r = Some (vrest ++ p') -> Forward ((x :: xx :: rrest) ++ input2) (y :: r) = Some ((Select x :: vrest) ++ p')p': prog
input1: list nat
x, xx: nat
rrest: list nat
input1eq: input1 = x :: xx :: rrest
Ih: forall y : list nat, length y < length (x :: xx :: rrest) -> forall (p : prog) (input2 output : list nat), Forward y output = Some p -> Forward input2 nil = Some p' -> Forward (y ++ input2) output = Some (p ++ p')
p: prog
input2: list nat
y: nat
r: list nat
rrestlt: length rrest < length (x :: xx :: rrest)
restlt: length (xx :: rrest) < length (x :: xx :: rrest)
vrest: prog
eqnrest: Forward (xx :: rrest) r = Some vrest
xeqy: (x =? y) = true
v2: Forward input2 nil = Some p'match r with | nil => match rrest ++ input2 with | nil => None | _ :: rrest => match Forward rrest nil with | Some pp => Some (Select xx :: Backspace :: pp) | None => None end end | y :: r0 => if xx =? y then match Forward (rrest ++ input2) r0 with | Some pp => Some (Select xx :: pp) | None => None end else match rrest ++ input2 with | nil => None | _ :: rrest => match Forward rrest r with | Some pp => Some (Select xx :: Backspace :: pp) | None => None end end end = Some (vrest ++ p') -> (if x =? y then match match r with | nil => match rrest ++ input2 with | nil => None | _ :: rrest => match Forward rrest nil with | Some pp => Some (Select xx :: Backspace :: pp) | None => None end end | y :: r0 => if xx =? y then match Forward (rrest ++ input2) r0 with | Some pp => Some (Select xx :: pp) | None => None end else match rrest ++ input2 with | nil => None | _ :: rrest => match Forward rrest r with | Some pp => Some (Select xx :: Backspace :: pp) | None => None end end end with | Some pp => Some (Select x :: pp) | None => None end else match Forward (rrest ++ input2) (y :: r) with | Some pp => Some (Select x :: Backspace :: pp) | None => None end) = Some (Select x :: vrest ++ p')p': prog
input1: list nat
x, xx: nat
rrest: list nat
input1eq: input1 = x :: xx :: rrest
Ih: forall y : list nat, length y < length (x :: xx :: rrest) -> forall (p : prog) (input2 output : list nat), Forward y output = Some p -> Forward input2 nil = Some p' -> Forward (y ++ input2) output = Some (p ++ p')
p: prog
input2: list nat
y: nat
r: list nat
rrestlt: length rrest < length (x :: xx :: rrest)
restlt: length (xx :: rrest) < length (x :: xx :: rrest)
vrest: prog
eqnrest: Forward (xx :: rrest) r = Some vrest
xeqy: (x =? y) = true
v2: Forward input2 nil = Some p'match r with | nil => match rrest ++ input2 with | nil => None | _ :: rrest => match Forward rrest nil with | Some pp => Some (Select xx :: Backspace :: pp) | None => None end end | y :: r0 => if xx =? y then match Forward (rrest ++ input2) r0 with | Some pp => Some (Select xx :: pp) | None => None end else match rrest ++ input2 with | nil => None | _ :: rrest => match Forward rrest r with | Some pp => Some (Select xx :: Backspace :: pp) | None => None end end end = Some (vrest ++ p') -> match match r with | nil => match rrest ++ input2 with | nil => None | _ :: rrest => match Forward rrest nil with | Some pp => Some (Select xx :: Backspace :: pp) | None => None end end | y :: r0 => if xx =? y then match Forward (rrest ++ input2) r0 with | Some pp => Some (Select xx :: pp) | None => None end else match rrest ++ input2 with | nil => None | _ :: rrest => match Forward rrest r with | Some pp => Some (Select xx :: Backspace :: pp) | None => None end end end with | Some pp => Some (Select x :: pp) | None => None end = Some (Select x :: vrest ++ p')p': prog
input1: list nat
x, xx: nat
rrest: list nat
input1eq: input1 = x :: xx :: rrest
Ih: forall y : list nat, length y < length (x :: xx :: rrest) -> forall (p : prog) (input2 output : list nat), Forward y output = Some p -> Forward input2 nil = Some p' -> Forward (y ++ input2) output = Some (p ++ p')
p: prog
input2: list nat
y: nat
r: list nat
rrestlt: length rrest < length (x :: xx :: rrest)
restlt: length (xx :: rrest) < length (x :: xx :: rrest)
vrest: prog
eqnrest: Forward (xx :: rrest) r = Some vrest
xeqy: (x =? y) = true
v2: Forward input2 nil = Some p'
it: match r with | nil => match rrest ++ input2 with | nil => None | _ :: rrest => match Forward rrest nil with | Some pp => Some (Select xx :: Backspace :: pp) | None => None end end | y :: r0 => if xx =? y then match Forward (rrest ++ input2) r0 with | Some pp => Some (Select xx :: pp) | None => None end else match rrest ++ input2 with | nil => None | _ :: rrest => match Forward rrest r with | Some pp => Some (Select xx :: Backspace :: pp) | None => None end end end = Some (vrest ++ p')match match r with | nil => match rrest ++ input2 with | nil => None | _ :: rrest => match Forward rrest nil with | Some pp => Some (Select xx :: Backspace :: pp) | None => None end end | y :: r0 => if xx =? y then match Forward (rrest ++ input2) r0 with | Some pp => Some (Select xx :: pp) | None => None end else match rrest ++ input2 with | nil => None | _ :: rrest => match Forward rrest r with | Some pp => Some (Select xx :: Backspace :: pp) | None => None end end end with | Some pp => Some (Select x :: pp) | None => None end = Some (Select x :: vrest ++ p')easy.p': prog
input1: list nat
x, xx: nat
rrest: list nat
input1eq: input1 = x :: xx :: rrest
Ih: forall y : list nat, length y < length (x :: xx :: rrest) -> forall (p : prog) (input2 output : list nat), Forward y output = Some p -> Forward input2 nil = Some p' -> Forward (y ++ input2) output = Some (p ++ p')
p: prog
input2: list nat
y: nat
r: list nat
rrestlt: length rrest < length (x :: xx :: rrest)
restlt: length (xx :: rrest) < length (x :: xx :: rrest)
vrest: prog
eqnrest: Forward (xx :: rrest) r = Some vrest
xeqy: (x =? y) = true
v2: Forward input2 nil = Some p'
it: match r with | nil => match rrest ++ input2 with | nil => None | _ :: rrest => match Forward rrest nil with | Some pp => Some (Select xx :: Backspace :: pp) | None => None end end | y :: r0 => if xx =? y then match Forward (rrest ++ input2) r0 with | Some pp => Some (Select xx :: pp) | None => None end else match rrest ++ input2 with | nil => None | _ :: rrest => match Forward rrest r with | Some pp => Some (Select xx :: Backspace :: pp) | None => None end end end = Some (vrest ++ p')Some (Select x :: vrest ++ p') = Some (Select x :: vrest ++ p')p': prog
input1: list nat
x, xx: nat
rrest: list nat
input1eq: input1 = x :: xx :: rrest
Ih: forall y : list nat, length y < length (x :: xx :: rrest) -> forall (p : prog) (input2 output : list nat), Forward y output = Some p -> Forward input2 nil = Some p' -> Forward (y ++ input2) output = Some (p ++ p')
p: prog
input2: list nat
y: nat
r: list nat
rrestlt: length rrest < length (x :: xx :: rrest)
restlt: length (xx :: rrest) < length (x :: xx :: rrest)
vrest: prog
eqnrest: Forward (xx :: rrest) r = Some vrest
xeqy: (x =? y) = falsematch Forward rrest (y :: r) with | Some pp => Some (Select x :: Backspace :: pp) | None => None end = Some p -> Forward input2 nil = Some p' -> Forward ((x :: xx :: rrest) ++ input2) (y :: r) = Some (p ++ p')p': prog
input1: list nat
x, xx: nat
rrest: list nat
input1eq: input1 = x :: xx :: rrest
Ih: forall y : list nat, length y < length (x :: xx :: rrest) -> forall (p : prog) (input2 output : list nat), Forward y output = Some p -> Forward input2 nil = Some p' -> Forward (y ++ input2) output = Some (p ++ p')
p: prog
input2: list nat
y: nat
r: list nat
rrestlt: length rrest < length (x :: xx :: rrest)
restlt: length (xx :: rrest) < length (x :: xx :: rrest)
vrest: prog
eqnrest: Forward (xx :: rrest) r = Some vrest
xeqy: (x =? y) = false
v: prog
eqnrrest: Forward rrest (y :: r) = Some vSome (Select x :: Backspace :: v) = Some p -> Forward input2 nil = Some p' -> Forward ((x :: xx :: rrest) ++ input2) (y :: r) = Some (p ++ p')p': prog
input1: list nat
x, xx: nat
rrest: list nat
input1eq: input1 = x :: xx :: rrest
Ih: forall y : list nat, length y < length (x :: xx :: rrest) -> forall (p : prog) (input2 output : list nat), Forward y output = Some p -> Forward input2 nil = Some p' -> Forward (y ++ input2) output = Some (p ++ p')
p: prog
input2: list nat
y: nat
r: list nat
rrestlt: length rrest < length (x :: xx :: rrest)
restlt: length (xx :: rrest) < length (x :: xx :: rrest)
vrest: prog
eqnrest: Forward (xx :: rrest) r = Some vrest
xeqy: (x =? y) = false
v: prog
eqnrrest: Forward rrest (y :: r) = Some v
vp: Select x :: Backspace :: v = p
v2: Forward input2 nil = Some p'Forward ((x :: xx :: rrest) ++ input2) (y :: r) = Some (p ++ p')p': prog
input1: list nat
x, xx: nat
rrest: list nat
input1eq: input1 = x :: xx :: rrest
Ih: forall y : list nat, length y < length (x :: xx :: rrest) -> forall (p : prog) (input2 output : list nat), Forward y output = Some p -> Forward input2 nil = Some p' -> Forward (y ++ input2) output = Some (p ++ p')
p: prog
input2: list nat
y: nat
r: list nat
rrestlt: length rrest < length (x :: xx :: rrest)
restlt: length (xx :: rrest) < length (x :: xx :: rrest)
vrest: prog
eqnrest: Forward (xx :: rrest) r = Some vrest
xeqy: (x =? y) = false
v: prog
eqnrrest: Forward rrest (y :: r) = Some v
vp: Select x :: Backspace :: v = p
v2: Forward input2 nil = Some p'Forward ((x :: xx :: rrest) ++ input2) (y :: r) = Some ((Select x :: Backspace :: v) ++ p')p': prog
input1: list nat
x, xx: nat
rrest: list nat
input1eq: input1 = x :: xx :: rrest
Ih: forall y : list nat, length y < length (x :: xx :: rrest) -> forall (p : prog) (input2 output : list nat), Forward y output = Some p -> Forward input2 nil = Some p' -> Forward (y ++ input2) output = Some (p ++ p')
p: prog
input2: list nat
y: nat
r: list nat
rrestlt: length rrest < length (x :: xx :: rrest)
restlt: length (xx :: rrest) < length (x :: xx :: rrest)
vrest: prog
eqnrest: Forward (xx :: rrest) r = Some vrest
xeqy: (x =? y) = false
v: prog
eqnrrest: Forward rrest (y :: r) = Some v
v2: Forward input2 nil = Some p'Forward ((x :: xx :: rrest) ++ input2) (y :: r) = Some ((Select x :: Backspace :: v) ++ p')p': prog
input1: list nat
x, xx: nat
rrest: list nat
input1eq: input1 = x :: xx :: rrest
Ih: forall y : list nat, length y < length (x :: xx :: rrest) -> forall (p : prog) (input2 output : list nat), Forward y output = Some p -> Forward input2 nil = Some p' -> Forward (y ++ input2) output = Some (p ++ p')
p: prog
input2: list nat
y: nat
r: list nat
rrestlt: length rrest < length (x :: xx :: rrest)
restlt: length (xx :: rrest) < length (x :: xx :: rrest)
vrest: prog
eqnrest: Forward (xx :: rrest) r = Some vrest
xeqy: (x =? y) = false
v: prog
eqnrrest: Forward rrest (y :: r) = Some v
v2: Forward input2 nil = Some p'(if x =? y then match match r with | nil => match rrest ++ input2 with | nil => None | _ :: rrest => match Forward rrest nil with | Some pp => Some (Select xx :: Backspace :: pp) | None => None end end | y :: r0 => if xx =? y then match Forward (rrest ++ input2) r0 with | Some pp => Some (Select xx :: pp) | None => None end else match rrest ++ input2 with | nil => None | _ :: rrest => match Forward rrest r with | Some pp => Some (Select xx :: Backspace :: pp) | None => None end end end with | Some pp => Some (Select x :: pp) | None => None end else match Forward (rrest ++ input2) (y :: r) with | Some pp => Some (Select x :: Backspace :: pp) | None => None end) = Some (Select x :: Backspace :: v ++ p')easy.p': prog
input1: list nat
x, xx: nat
rrest: list nat
input1eq: input1 = x :: xx :: rrest
Ih: forall y : list nat, length y < length (x :: xx :: rrest) -> forall (p : prog) (input2 output : list nat), Forward y output = Some p -> Forward input2 nil = Some p' -> Forward (y ++ input2) output = Some (p ++ p')
p: prog
input2: list nat
y: nat
r: list nat
rrestlt: length rrest < length (x :: xx :: rrest)
restlt: length (xx :: rrest) < length (x :: xx :: rrest)
vrest: prog
eqnrest: Forward (xx :: rrest) r = Some vrest
xeqy: (x =? y) = false
v: prog
eqnrrest: Forward rrest (y :: r) = Some v
v2: Forward input2 nil = Some p'Some (Select x :: Backspace :: v ++ p') = Some (Select x :: Backspace :: v ++ p')p': prog
input1: list nat
x, xx: nat
rrest: list nat
input1eq: input1 = x :: xx :: rrest
Ih: forall y : list nat, length y < length (x :: xx :: rrest) -> forall (p : prog) (input2 output : list nat), Forward y output = Some p -> Forward input2 nil = Some p' -> Forward (y ++ input2) output = Some (p ++ p')
p: prog
input2: list nat
y: nat
r: list nat
rrestlt: length rrest < length (x :: xx :: rrest)
restlt: length (xx :: rrest) < length (x :: xx :: rrest)
eqnrest: Forward (xx :: rrest) r = None(if x =? y then None else match Forward rrest (y :: r) with | Some pp => Some (Select x :: Backspace :: pp) | None => None end) = Some p -> Forward input2 nil = Some p' -> Forward ((x :: xx :: rrest) ++ input2) (y :: r) = Some (p ++ p')p': prog
input1: list nat
x, xx: nat
rrest: list nat
input1eq: input1 = x :: xx :: rrest
Ih: forall y : list nat, length y < length (x :: xx :: rrest) -> forall (p : prog) (input2 output : list nat), Forward y output = Some p -> Forward input2 nil = Some p' -> Forward (y ++ input2) output = Some (p ++ p')
p: prog
input2: list nat
y: nat
r: list nat
rrestlt: length rrest < length (x :: xx :: rrest)
restlt: length (xx :: rrest) < length (x :: xx :: rrest)
eqnrest: Forward (xx :: rrest) r = None
xeqy: (x =? y) = falsematch Forward rrest (y :: r) with | Some pp => Some (Select x :: Backspace :: pp) | None => None end = Some p -> Forward input2 nil = Some p' -> Forward ((x :: xx :: rrest) ++ input2) (y :: r) = Some (p ++ p')p': prog
input1: list nat
x, xx: nat
rrest: list nat
input1eq: input1 = x :: xx :: rrest
Ih: forall y : list nat, length y < length (x :: xx :: rrest) -> forall (p : prog) (input2 output : list nat), Forward y output = Some p -> Forward input2 nil = Some p' -> Forward (y ++ input2) output = Some (p ++ p')
p: prog
input2: list nat
y: nat
r: list nat
rrestlt: length rrest < length (x :: xx :: rrest)
restlt: length (xx :: rrest) < length (x :: xx :: rrest)
eqnrest: Forward (xx :: rrest) r = None
xeqy: (x =? y) = false
v: prog
eqnrrest: Forward rrest (y :: r) = Some vSome (Select x :: Backspace :: v) = Some p -> Forward input2 nil = Some p' -> Forward ((x :: xx :: rrest) ++ input2) (y :: r) = Some (p ++ p')p': prog
input1: list nat
x, xx: nat
rrest: list nat
input1eq: input1 = x :: xx :: rrest
Ih: forall y : list nat, length y < length (x :: xx :: rrest) -> forall (p : prog) (input2 output : list nat), Forward y output = Some p -> Forward input2 nil = Some p' -> Forward (y ++ input2) output = Some (p ++ p')
p: prog
input2: list nat
y: nat
r: list nat
rrestlt: length rrest < length (x :: xx :: rrest)
restlt: length (xx :: rrest) < length (x :: xx :: rrest)
eqnrest: Forward (xx :: rrest) r = None
xeqy: (x =? y) = false
v: prog
eqnrrest: Forward rrest (y :: r) = Some v
vp: Select x :: Backspace :: v = p
v2: Forward input2 nil = Some p'Forward ((x :: xx :: rrest) ++ input2) (y :: r) = Some (p ++ p')p': prog
input1: list nat
x, xx: nat
rrest: list nat
input1eq: input1 = x :: xx :: rrest
Ih: forall y : list nat, length y < length (x :: xx :: rrest) -> forall (p : prog) (input2 output : list nat), Forward y output = Some p -> Forward input2 nil = Some p' -> Forward (y ++ input2) output = Some (p ++ p')
p: prog
input2: list nat
y: nat
r: list nat
rrestlt: length rrest < length (x :: xx :: rrest)
restlt: length (xx :: rrest) < length (x :: xx :: rrest)
eqnrest: Forward (xx :: rrest) r = None
xeqy: (x =? y) = false
v: prog
eqnrrest: Forward rrest (y :: r) = Some v
vp: Select x :: Backspace :: v = p
v2: Forward input2 nil = Some p'Forward ((x :: xx :: rrest) ++ input2) (y :: r) = Some ((Select x :: Backspace :: v) ++ p')p': prog
input1: list nat
x, xx: nat
rrest: list nat
input1eq: input1 = x :: xx :: rrest
Ih: forall y : list nat, length y < length (x :: xx :: rrest) -> forall (p : prog) (input2 output : list nat), Forward y output = Some p -> Forward input2 nil = Some p' -> Forward (y ++ input2) output = Some (p ++ p')
p: prog
input2: list nat
y: nat
r: list nat
rrestlt: length rrest < length (x :: xx :: rrest)
restlt: length (xx :: rrest) < length (x :: xx :: rrest)
eqnrest: Forward (xx :: rrest) r = None
xeqy: (x =? y) = false
v: prog
eqnrrest: Forward rrest (y :: r) = Some v
v2: Forward input2 nil = Some p'Forward ((x :: xx :: rrest) ++ input2) (y :: r) = Some ((Select x :: Backspace :: v) ++ p')p': prog
input1: list nat
x, xx: nat
rrest: list nat
input1eq: input1 = x :: xx :: rrest
Ih: forall y : list nat, length y < length (x :: xx :: rrest) -> forall (p : prog) (input2 output : list nat), Forward y output = Some p -> Forward input2 nil = Some p' -> Forward (y ++ input2) output = Some (p ++ p')
p: prog
input2: list nat
y: nat
r: list nat
rrestlt: length rrest < length (x :: xx :: rrest)
restlt: length (xx :: rrest) < length (x :: xx :: rrest)
eqnrest: Forward (xx :: rrest) r = None
xeqy: (x =? y) = false
v: prog
eqnrrest: Forward rrest (y :: r) = Some v
v2: Forward input2 nil = Some p'(if x =? y then match match r with | nil => match rrest ++ input2 with | nil => None | _ :: rrest => match Forward rrest nil with | Some pp => Some (Select xx :: Backspace :: pp) | None => None end end | y :: r0 => if xx =? y then match Forward (rrest ++ input2) r0 with | Some pp => Some (Select xx :: pp) | None => None end else match rrest ++ input2 with | nil => None | _ :: rrest => match Forward rrest r with | Some pp => Some (Select xx :: Backspace :: pp) | None => None end end end with | Some pp => Some (Select x :: pp) | None => None end else match Forward (rrest ++ input2) (y :: r) with | Some pp => Some (Select x :: Backspace :: pp) | None => None end) = Some (Select x :: Backspace :: v ++ p')easy. Qed.p': prog
input1: list nat
x, xx: nat
rrest: list nat
input1eq: input1 = x :: xx :: rrest
Ih: forall y : list nat, length y < length (x :: xx :: rrest) -> forall (p : prog) (input2 output : list nat), Forward y output = Some p -> Forward input2 nil = Some p' -> Forward (y ++ input2) output = Some (p ++ p')
p: prog
input2: list nat
y: nat
r: list nat
rrestlt: length rrest < length (x :: xx :: rrest)
restlt: length (xx :: rrest) < length (x :: xx :: rrest)
eqnrest: Forward (xx :: rrest) r = None
xeqy: (x =? y) = false
v: prog
eqnrrest: Forward rrest (y :: r) = Some v
v2: Forward input2 nil = Some p'Some (Select x :: Backspace :: v ++ p') = Some (Select x :: Backspace :: v ++ p')A careful scrutiny of the script for lemma app_forward2 shows that the script is almost the same as for app_forward. Three main hints:
well_founded_induction combined with wf_inverse_image, length and lt_wf gives a general induction hypothesis that can be use for every case where input1 is replaced with a list that is shorter in length.
destruct input1 replaces every instance of input1 with a variety of cases, including the instance that appears in the induction hypothesis.
all calls to induction hypotheses Ih1 and Ih2 in the previous solution have simply been replaced by calls to Ih, using hypotheses restlt and rrestlt to guarantee length decrease.