Coq simpl / unfold only once. (Replace part of goal with the result of one iteration of a function.)

Question

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)

Breaker

Answer 1

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.

Revere

Answer 2

I'm not sure there is a way to do it right off the bat. One usual way is to prove a lemma corresponding the computation rule by reflexivity:

Lemma greaterThan_suc_suc :
  forall n m,
    suc n > suc m = n > m.
Proof.
  intros. reflexivity.
Defined.

(I'm using defined so that it really unfolds to eq_refl and goes away if need be.)

There is also the possibility of doing a change to do a substitution manually.

change (suc (suc t) > suc t) with (suc t > t).

It will check for convertibility and replace one expression by the other in the goal.

You can automate this process a bit by writing a tactic that does the simplification.

Ltac red_greaterThan :=
  match goal with
  | |- context [ suc ?n > suc ?m ] =>
    change (suc n > suc m) with (n > m)
  | |- context [ suc ?n > zero ] =>
    change (suc n > zero) with true
  | |- context [ zero > ?n ] =>
    change (zero > n) with false
  end.

Lemma successorIsGreater : forall t : term, suc t > t = true.
Proof.
  induction t.

  (* zero *)
  - red_greaterThan. reflexivity.

  (* suc t *)
  - red_greaterThan. assumption.
Qed.

Subaqueous

Though it's not exactly what I was looking for (since they are convertible, I could use exact by itself as well, which doesn't show the procedure to the students), change still seems to be my best bet, so thank you very much for mentioning that possibility! I will mark your answer to be the accepted if no better one arrives. – Breaker

I hope someone does. I'd be glad as well. I'll update my answer with something more. – Cf

Thank you for the updated content, I really appreciate it! At last I've marked SCappella's answer as accepted, as it seems better suited for what I was looking for (requires less explanation), but there are great things to keep in mind as possibilities as well! – Breaker