I am an instructor at university for a class titled Type Systems of Languages and the professor used the following example for inductive proofs in Type Theory on the board last lecture:
Suppose, that there are natural numbers defined inductively (for some reason he insists on calling them terms) and we have a greater than function defined recursively on them. We can proove that for every n it holds that (suc n > n).
I have the following Coq code prepared for implementing this in a class:
Inductive term : Set :=
| zero
| suc (t : term)
.
Fixpoint greaterThan (t t' : term) {struct t} : bool :=
match t, t' with
| zero, _ => false
| suc t, zero => true
| suc t, suc t' => t > t'
end
where "t > t'" := (greaterThan t t').
Lemma successorIsGreater : forall t : term, suc t > t = true.
Proof.
induction t.
(* zero *)
- simpl.
reflexivity.
(* suc t *)
-
which takes me to the following goal:
1 subgoal
t : term
IHt : (suc t > t) = true
______________________________________(1/1)
(suc (suc t) > suc t) = true
I can solve this in multiple ways by rewriting, unfolding, and / or simplifying before it just turns into reflexivity, but what I would really like to do to make it cleaner is to apply one iteration of greaterThan, that would just turn (suc (suc t) > suc t) = true into (suc t > t) = true, and I could finish the proof with exact IHt.
Is there a way to ahieve this?
ps.: I know that I can simpl in IHt and then use exact, but it expands to the match expression which is much more verbose than what is neccessary here.
Edit: Thanks to Théo Winterhalter's answer I realized that I could also use exact by itself, since the terms are convertible, but that wouldn't show the process too well to the students. (Side note: Both cases of the induction are solvable with trivial as well, but I don't think that they would learn too much from that either. :D)
Another possibility is to use the Arguments vernacular to tell simpl not to reduce greaterThan to a match expression. Put Arguments greaterThan: simpl nomatch. somewhere after the definition of greaterThan. Then when you use simpl in the environment
1 subgoal
t : term
IHt : (suc t > t) = true
______________________________________(1/1)
(suc (suc t) > suc t) = true
you get
1 subgoal
t : term
IHt : (suc t > t) = true
______________________________________(1/1)
(suc t > t) = true
as you wanted.