Skip to content

Instantly share code, notes, and snippets.

@gallais
Created May 22, 2020
Embed
What would you like to do?
Palindrome via an accumulator-based definition.
Require Import List.
Inductive PalAcc {A : Type} (acc : list A) : list A -> Type
:= Even : PalAcc acc acc
| Odd : forall x, PalAcc acc (x :: acc)
| Step : forall x xs, PalAcc (x :: acc) xs -> PalAcc acc (x :: xs)
.
Definition Pal {A : Type} (xs : list A) : Type := PalAcc nil xs.
Theorem PalAccRevAcc {A : Type} (acc xs : list A) :
PalAcc acc xs -> rev_append acc xs = rev_append xs acc.
Proof.
induction 1; trivial.
Qed.
Theorem PalRev {A : Type} (xs : list A) :
Pal xs -> rev xs = xs.
Proof.
intro prf; rewrite rev_alt, <- (PalAccRevAcc _ _ prf); reflexivity.
Qed.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment