How to be bad at coq if you know idris

  • Ability to fulfill obligations.
  • Ability to dismiss obligations that are impossible (using dependencies between proofs).
  • Ability to apply induction.
Fixpoint nat_lt (a : nat) (b : nat) : bool :=
match b with
| 0 => false
| (S b1) =>
match a with
| 0 => true
| (S a1) => nat_lt a1 b1
end
end.
Lemma zero_zero_lt : nat_lt 0 0 = false.                             Proof.
reflexivity.
Qed.
  • The bound variables held by the prover.
  • A stack of state machines that provide the next goal.
Lemma two_lt_n_means_1_lt_n (n : nat) (p : nat_lt 2 n = true) : nat_lt 1 n = true.
Proof.
intros.
case_eq n. (* push n = 0 and n = S n0 as variant proof goals *)
eintros. (* bind H: n = 0 and n: 0 *)
rewrite H in p. (* H is a hypothesis bound above, n = 0 *)
(* any_lt_zero x -> nat_lt (S x) 0 = false *)
rewrite (any_lt_zero 1) in p.
(* if any proof in scope is a contradiction, dismiss this goal. *)
discriminate.
intros.
case_eq n0.
intros. (* bind n0 = 0 *)
rewrite H in p.
rewrite H0 in p.
simpl in p.
discriminate.
intros.
simpl.
reflexivity.
Qed.
rewrite (any_lt_zero 1) in p.
p : nat_lt 2 0 = true
p : false = true
discriminate.
2 goals
n : nat
p : false = true
H : n = 0
______________________________________(1/2)
nat_lt 1 0 = true
______________________________________(2/2)
forall n0 : nat, n = S n0 -> nat_lt 1 (S n0) = true
1 goal
n : nat
p : nat_lt 2 n = true
______________________________________(1/1)
forall n0 : nat, n = S n0 -> nat_lt 1 (S n0) = true

--

--

Get the Medium app

A button that says 'Download on the App Store', and if clicked it will lead you to the iOS App store
A button that says 'Get it on, Google Play', and if clicked it will lead you to the Google Play store