Permalink
Browse files

update before class

  • Loading branch information...
1 parent 30568e0 commit 909a048f1354262c31265f8520a4c90b2bacac29 @Janno committed Apr 25, 2012
Showing with 19 additions and 2 deletions.
  1. +19 −2 ex1.v
View
@@ -79,18 +79,35 @@ Section Ex1.
(* We define total computable functions to be
reducible partial computable functions. *)
+ Record tcfunction' : Type :=
+ tcfuncI' {
+ tcfunc' :> pcfunction;
+ tcreducible' : reducible tcfunc'
+ }.
+
+ (* We give an equivalent definition and only use that
+ from here on. *)
Record tcfunction : Type :=
tcfuncI {
- tcfunc :> pcfunction;
- tcreducible : reducible tcfunc
+ tcfunc :> func
}.
+ Lemma tcf_1 : tcfunction -> tcfunction'.
+ Proof.
+ intros f.
+ pose (f' := fun x y => f x = y).
+ assert (forall x y, f x = f y -> x = y).
+
+ apply (tcfuncI' f').
+ Lemma tcf_2: tcfunction' -> tcfunction.
+
(* We define a coercion from total computable
functions to normal Coq functions. *)
Definition tcf (f: tcfunction) : nat -> nat.
intros x. destruct (tcreducible f x). exact x0. Defined.
+
(* We define the type of turing machines to
be the natural numbers, i.e. we only deal
with encoded turing machines.

0 comments on commit 909a048

Please sign in to comment.