Skip to content

Instantly share code, notes, and snippets.

@dcci dcci/indprop.v
Created Mar 7, 2018

Embed
What would you like to do?
Inductively defined propositions in coq
Inductive ev : nat -> Prop :=
| ev_0 : ev 0
| ev_SS : forall n : nat, ev n -> ev (S (S n)).
Theorem ev_4 : ev 4.
Proof.
apply ev_SS.
apply ev_SS.
apply ev_0.
Qed.
Theorem ev_4' : ev 4.
Proof.
apply (ev_SS 2 (ev_SS 0 ev_0)).
Qed.
Theorem ev_plus4 : forall n, ev n -> ev (4 + n).
Proof.
intros n H.
apply ev_SS.
apply ev_SS.
apply H.
Qed.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.