So now I've got this, but have a little problem interpreting the error message.
Error: Abstracting over the term "type 0" leads to a term
"fun P : Set => tZ P getn" which is ill-typed.
Inductive type : nat -> Set := ctor : forall n, type n.
Definition tZ X f := forall x : X, f x = 0.
Definition getn {n} (x : type n) := n.
Lemma tZO : tZ (type 0) getn. compute. auto. Qed.
Lemma tZS : forall n, ~tZ (type (S n)) getn. intro. intro. compute in H. assert (Hx := H (ctor (S n))). discriminate. Qed.
Require Import Setoid.
Goal forall n, type 0 <> type (S n). intro. intro. assert (HO := tZO). assert (HS := tZS n). rewrite H in HO.
Wizards of the coed halp plox111 How do I make my coq to accept this?
Definition fb (x : bool) : Set := nat.
Definition fn (x : nat) : Set := nat.
Definition depx (b : bool) (x : if b then bool else nat) (y : if b then fb x else fn x) := 0.
My coq accepts lots of things, so there might be something wrong with your coq.
Name:
Anonymous2012-05-19 15:09
>>10 Definition fb (x : bool) : Set := nat.
Definition fn (x : nat) : Set := nat.
(* New decision procedure because bool_dec is annoying. *)
Lemma bool_true_false (b : bool) : {b = true} + {b = false}.
destruct b.
left. reflexivity.
right. reflexivity.
Defined.
(* Print bool_true_false. *)
Definition bool_or_nat (b : bool) := if b then bool else nat.
(* Use eq_rect to convert "x : bool_or_nat b" to "x : bool_or_nat true" using "b = true" *)
Definition depx
(b : bool)
(x : bool_or_nat b)
(y : match bool_true_false b with
| left H => fb (eq_rect b bool_or_nat x true H)
| right H => fn (eq_rect b bool_or_nat x false H)
end)
:= 0.
Name:
Anonymous2012-05-19 16:18
suck my coq
Name:
Anonymous2012-05-19 20:00
>>12
Thanks anon, you are a Gentleman and a Scholar!
I am offended by the usage of sexual humour in this thread on a public programming board. It is inappropriate and it creates a hostile environment to women.
Name:
Anonymous2013-06-20 8:09
you can't, this is independent of Coq
you can only disprove a <> b for a,b : Set if they have a different number of elements.