(* We inductively define the set of terms *) Inductive term : Set := | squiggle : term -> term | squaggle : term -> term | sqop : term | transmogrify : term -> term -> term. Section Exercise1. (* Syntax We check if the following expressions are indeed terms. *) Check squiggle sqop : term. (*Check sqop sqop : term.*) (*Check transmogrify (squiggle squaggle) squiggle : term.*) Check squiggle (squaggle sqop) : term. Section Exercise2. (* Inference rules We define inference rules*) Inductive Inference_Rule : term -> Prop := | I_squiggle : forall t : term, Inference_Rule t -> Inference_Rule (squiggle t) | I_squaggle : forall t : term, Inference_Rule t -> Inference_Rule (squaggle t) | I_sqop : Inference_Rule sqop | I_transmogrify : forall t1 : term, forall t2 : term, Inference_Rule t1 -> Inference_Rule t2 -> Inference_Rule (transmogrify t1 t2). Section Exercise3. (* Induction We inductively define the relation C i t of terms t with maximum depth i. *) Inductive C : nat -> term -> Prop := | C_squiggle : forall i : nat, forall t : term, C i t -> C (1 + i) (squiggle t) | C_squaggle : forall i : nat, forall t : term, C i t -> C (1 + i) (squaggle t) | C_sqop : forall i : nat, C (1 + i) sqop | C_transmogrify : forall i : nat, forall t1 : term, forall t2 : term, C i t1 -> C i t2 -> C (1 + i) (transmogrify t1 t2). Lemma C_cumulative : forall i : nat, forall t : term, C i t -> C (1 + i) t. intros i t c. induction c. apply C_squiggle. exact IHc. apply C_squaggle. exact IHc. apply C_sqop. apply C_transmogrify. exact IHc1. exact IHc2. Qed. End Exercise3.