Mercurial > cpdt > repo

comparison src/Subset.v @ 380:31fa03bc0f18

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Get it to build with Coq 8.4
author Adam Chlipala <adam@chlipala.net>
date Thu, 29 Mar 2012 18:10:52 -0400
parents 549d604c3d16
children 4b1242b277b2
comparison
equal deleted inserted replaced
379:e23d41ae63be 380:31fa03bc0f18
1 (* Copyright (c) 2008-2011, Adam Chlipala 1 (* Copyright (c) 2008-2012, Adam Chlipala
2 * 2 *
3 * This work is licensed under a 3 * This work is licensed under a
4 * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0 4 * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
5 * Unported License. 5 * Unported License.
6 * The license text is available at: 6 * The license text is available at:
564 564
565 (** Now our next version of [pred] is trivial to write. *) 565 (** Now our next version of [pred] is trivial to write. *)
566 566
567 Definition pred_strong7 : forall n : nat, {{m | n = S m}}. 567 Definition pred_strong7 : forall n : nat, {{m | n = S m}}.
568 refine (fun n => 568 refine (fun n =>
569 match n with 569 match n return {{m | n = S m}} with
570 | O => ?? 570 | O => ??
571 | S n' => [|n'|] 571 | S n' => [|n'|]
572 end); trivial. 572 end); trivial.
573 Defined. 573 Defined.
574 574
723 Definition typeCheck : forall e : exp, {{t | hasType e t}}. 723 Definition typeCheck : forall e : exp, {{t | hasType e t}}.
724 (* begin thide *) 724 (* begin thide *)
725 Hint Constructors hasType. 725 Hint Constructors hasType.
726 726
727 refine (fix F (e : exp) : {{t | hasType e t}} := 727 refine (fix F (e : exp) : {{t | hasType e t}} :=
728 match e with 728 match e return {{t | hasType e t}} with
729 | Nat _ => [|TNat|] 729 | Nat _ => [|TNat|]
730 | Plus e1 e2 => 730 | Plus e1 e2 =>
731 t1 <- F e1; 731 t1 <- F e1;
732 t2 <- F e2; 732 t2 <- F e2;
733 eq_type_dec t1 TNat;; 733 eq_type_dec t1 TNat;;
870 (** The lemma [hasType_det] will also be useful for proving proof obligations with contradictory contexts. Since its statement includes [forall]-bound variables that do not appear in its conclusion, only [eauto] will apply this hint. *) 870 (** The lemma [hasType_det] will also be useful for proving proof obligations with contradictory contexts. Since its statement includes [forall]-bound variables that do not appear in its conclusion, only [eauto] will apply this hint. *)
871 871
872 (** Finally, the implementation of [typeCheck] can be transcribed literally, simply switching notations as needed. *) 872 (** Finally, the implementation of [typeCheck] can be transcribed literally, simply switching notations as needed. *)
873 873
874 refine (fix F (e : exp) : {t : type | hasType e t} + {forall t, ~ hasType e t} := 874 refine (fix F (e : exp) : {t : type | hasType e t} + {forall t, ~ hasType e t} :=
875 match e with 875 match e return {t : type | hasType e t} + {forall t, ~ hasType e t} with
876 | Nat _ => [||TNat||] 876 | Nat _ => [||TNat||]
877 | Plus e1 e2 => 877 | Plus e1 e2 =>
878 t1 <-- F e1; 878 t1 <-- F e1;
879 t2 <-- F e2; 879 t2 <-- F e2;
880 eq_type_dec t1 TNat;;; 880 eq_type_dec t1 TNat;;;