Skip to content

Instantly share code, notes, and snippets.

@dcci

dcci/indprop.v

Created March 7, 2018 04:01
Show Gist options
  • Save dcci/8084a3f3ac6068d64febf0f062bb029f to your computer and use it in GitHub Desktop.
Save dcci/8084a3f3ac6068d64febf0f062bb029f to your computer and use it in GitHub Desktop.
Download ZIP
Inductively defined propositions in coq
Raw
indprop.v
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