I am trying to proof that the application of an empty Substitution on a term is equal to the given term. Here is the code:
Require Import Coq.Strings.String.
Require Import Coq.Lists.List.
Require Import Coq.Arith.EqNat.
Require Import Recdef.
Require Import Omega.
Import ListNotations.
Set Implicit Arguments.
Inductive Term : Type :=
| Var : nat -> Term
| Fun : string -> list Term -> Term.
Definition Subst : Type := list (nat*Term).
Definition maybe{X Y: Type} (x : X) (f : Y -> X) (o : option Y): X :=
match o with
|None => x
|Some a => f a
end.
Fixpoint lookup {A B : Type} (eqA : A -> A -> bool) (kvs : list (A * B)) (k : A) : option B :=
match kvs with
|[] => None
|(x,y) :: xs => if eqA k x then Some y else lookup eqA xs k
end.
I am trying to proof some properties of this function.
Fixpoint apply (s : Subst) (t : Term) : Term :=
match t with
| Var x => maybe (Var x) id (lookup beq_nat s x )
| Fun f ts => Fun f (map (apply s ) ts)
end.
Lemma empty_apply_on_term:
forall t, apply [] t = t.
Proof.
intros.
induction t.
reflexivity.
I am stuck after the reflexivity. I wanted to do induction on the list build in a term but if i do so i'ĺl get stuck in a loop. i will appreciate any help.