Self-evaluation 2

Authors:

Yannick Forster

Théo Winterhalter

Files:

Source

Display all goals and responses

Exercise 1

Write down the induction principle of expr.

Inductive expr (X : Type) :=
| var (x : X)
| add : expr X -> expr X -> expr X.

Exercise 2

Prove the following:

Goal forall X x e1 e2, var X x <> add X e1 e2.forall (X : Type) (x : X) (e1 e2 : expr X), var X x <> add X e1 e2

Exercise 3

Given the following inductive type, identify parameters, non-uniform parameters, and indices:

Inductive lt X (s : X -> X) (x : X) : X -> Prop :=
| lt_start : lt X s x (s x)
| le_S y : lt X s (s x) y -> lt X s x y.forall (X : Type) (x : X) (e1 e2 : expr X), var X x <> add X e1 e2

Exercise 4

Lemma lt_s_both X s x y :
  lt X s x y -> lt X s (s x) (s y).X: Type
s: X -> X
x, y: X
lt X s x y -> lt X s (s x) (s y)
Proof.X: Type
s: X -> X
x, y: X
lt X s x y -> lt X s (s x) (s y)
  induction 1 as [ | y h ih].X: Type
s: X -> X
x: X
lt X s (s x) (s (s x))
X: Type
s: X -> X
y, h: X
ih: lt X s (s y) h
IHih: lt X s (s (s y)) (s h)
lt X s (s y) (s h)
  -X: Type
s: X -> X
x: X
lt X s (s x) (s (s x)) constructor.
  -X: Type
s: X -> X
y, h: X
ih: lt X s (s y) h
IHih: lt X s (s (s y)) (s h)
lt X s (s y) (s h) (* what is the full goal here? give the types of
       every variable in the assumptions
       and the proof obligation
    *)