Last active
December 1, 2017 14:39
-
-
Save Isweet/ec9423def14841aebf119020f75164bd to your computer and use it in GitHub Desktop.
Using `refine` tactic to generate subgoals, but Coq complains when solving subgoals.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Inductive ev_dumb : nat -> Prop := | |
| EvDBase : ev_dumb 0 | |
| EvDRec : forall n, ev_dumb n /\ n <> 1 -> ev_dumb (S (S n)). | |
Check ev_dumb_ind. | |
(* ev_dumb_ind | |
: forall P : nat -> Prop, | |
P 0 -> (forall n : nat, ev_dumb n /\ n <> 1 -> P (S (S n))) -> forall n : nat, ev_dumb n -> P n | |
*) | |
Lemma ev_dumb_ind' : | |
forall P : nat -> Prop, | |
P 0 -> | |
(forall n : nat, P n -> ev_dumb n /\ n <> 1 -> P (S (S n))) -> | |
forall n : nat, ev_dumb n -> P n. | |
Proof. | |
intros P H0 H1. | |
refine (fix F n e := | |
match e with | |
| EvDBase => _ | |
| EvDRec n Hn => _ | |
end). | |
- apply H0. | |
- apply H1. | |
apply F. | |
destruct Hn. | |
apply H. | |
apply Hn. | |
Qed. | |
(* Error: | |
Recursive definition of F is ill-formed. | |
In environment | |
P : nat -> Prop | |
H0 : P 0 | |
H1 : forall n : nat, P n -> ev_dumb n /\ n <> 1 -> P (S (S n)) | |
F : forall n : nat, ev_dumb n -> P n | |
n : nat | |
e : ev_dumb n | |
n0 : nat | |
Hn : ev_dumb n0 /\ n0 <> 1 | |
Recursive call to F has principal argument equal to "n0" instead of a subterm of "n". | |
Recursive definition is: | |
"fun (n : nat) (e : ev_dumb n) => | |
match e in (ev_dumb n0) return (P n0) with | |
| EvDBase => H0 | |
| EvDRec n0 Hn => H1 n0 (F n0 match Hn with | |
| conj H _ => H | |
end) Hn | |
end". | |
*) |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment