Mercurial > cpdt > repo

comparison src/Extensional.v @ 244:0400fa005d5a

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
New release
author Adam Chlipala <adamc@hcoop.net>
date Wed, 09 Dec 2009 14:12:33 -0500
parents 19902d0b6622
children 4293dd6912cd
comparison
equal deleted inserted replaced
243:b2c72c77ad47 244:0400fa005d5a
382 (* end thide *) 382 (* end thide *)
383 383
384 End STLC. 384 End STLC.
385 385
386 386
387 (** * A Pattern Compiler *)
388
389 Module PatMatch.
390 Module Source.
391 Inductive type : Type :=
392 | Unit : type
393 | Arrow : type -> type -> type
394 | Prod : type -> type -> type
395 | Sum : type -> type -> type.
396
397 Infix "-->" := Arrow (right associativity, at level 61).
398 Infix "++" := Sum (right associativity, at level 60).
399 Infix "**" := Prod (right associativity, at level 59).
400
401 Inductive pat : type -> list type -> Type :=
402 | PVar : forall t,
403 pat t (t :: nil)
404 | PPair : forall t1 t2 ts1 ts2,
405 pat t1 ts1
406 -> pat t2 ts2
407 -> pat (t1 ** t2) (ts1 ++ ts2)
408 | PInl : forall t1 t2 ts,
409 pat t1 ts
410 -> pat (t1 ++ t2) ts
411 | PInr : forall t1 t2 ts,
412 pat t2 ts
413 -> pat (t1 ++ t2) ts.
414
415 Implicit Arguments PVar [t].
416 Implicit Arguments PInl [t1 t2 ts].
417 Implicit Arguments PInr [t1 t2 ts].
418
419 Notation "##" := PVar (at level 70) : pat_scope.
420 Notation "[ p1 , p2 ]" := (PPair p1 p2) : pat_scope.
421 Notation "'Inl' p" := (PInl p) (at level 71) : pat_scope.
422 Notation "'Inr' p" := (PInr p) (at level 71) : pat_scope.
423
424 Bind Scope pat_scope with pat.
425 Delimit Scope pat_scope with pat.
426
427 Section vars.
428 Variable var : type -> Type.
429
430 Inductive exp : type -> Type :=
431 | Var : forall t,
432 var t
433 -> exp t
434
435 | EUnit : exp Unit
436
437 | App : forall t1 t2,
438 exp (t1 --> t2)
439 -> exp t1
440 -> exp t2
441 | Abs : forall t1 t2,
442 (var t1 -> exp t2)
443 -> exp (t1 --> t2)
444
445 | Pair : forall t1 t2,
446 exp t1
447 -> exp t2
448 -> exp (t1 ** t2)
449
450 | EInl : forall t1 t2,
451 exp t1
452 -> exp (t1 ++ t2)
453 | EInr : forall t1 t2,
454 exp t2
455 -> exp (t1 ++ t2)
456
457 | Case : forall t1 t2 (tss : list (list type)),
458 exp t1
459 -> (forall ts, member ts tss -> pat t1 ts)
460 -> (forall ts, member ts tss -> hlist var ts -> exp t2)
461 -> exp t2
462 -> exp t2.
463 End vars.
464
465 Definition Exp t := forall var, exp var t.
466
467 Implicit Arguments Var [var t].
468 Implicit Arguments EUnit [var].
469 Implicit Arguments App [var t1 t2].
470 Implicit Arguments Abs [var t1 t2].
471 Implicit Arguments Pair [var t1 t2].
472 Implicit Arguments EInl [var t1 t2].
473 Implicit Arguments EInr [var t1 t2].
474 Implicit Arguments Case [var t1 t2].
475
476 Notation "# v" := (Var v) (at level 70) : source_scope.
477
478 Notation "()" := EUnit : source_scope.
479
480 Infix "@" := App (left associativity, at level 77) : source_scope.
481 Notation "\ x , e" := (Abs (fun x => e)) (at level 78) : source_scope.
482
483 Notation "[ x , y ]" := (Pair x y) : source_scope.
484
485 Notation "'Inl' e" := (EInl e) (at level 71) : source_scope.
486 Notation "'Inr' e" := (EInr e) (at level 71) : source_scope.
487
488 Delimit Scope source_scope with source.
489 Bind Scope source_scope with exp.
490
491 Local Open Scope source_scope.
492
493 Fixpoint typeDenote (t : type) : Set :=
494 match t with
495 | Unit => unit
496 | t1 --> t2 => typeDenote t1 -> typeDenote t2
497 | t1 ** t2 => (typeDenote t1 * typeDenote t2)%type
498 | t1 ++ t2 => (typeDenote t1 + typeDenote t2)%type
499 end.
500
501 Fixpoint patDenote t ts (p : pat t ts)
502 : typeDenote t -> option (hlist typeDenote ts) :=
503 match p with
504 | PVar _ => fun v => Some (v ::: HNil)
505 | PPair _ _ _ _ p1 p2 => fun v =>
506 match patDenote p1 (fst v), patDenote p2 (snd v) with
507 | Some tup1, Some tup2 => Some (happ tup1 tup2)
508 | _, _ => None
509 end
510 | PInl _ _ _ p' => fun v =>
511 match v with
512 | inl v' => patDenote p' v'
513 | _ => None
514 end
515 | PInr _ _ _ p' => fun v =>
516 match v with
517 | inr v' => patDenote p' v'
518 | _ => None
519 end
520 end.
521
522 Section matchesDenote.
523 Variables t2 : type.
524 Variable default : typeDenote t2.
525
526 Fixpoint matchesDenote (tss : list (list type))
527 : (forall ts, member ts tss -> option (hlist typeDenote ts))
528 -> (forall ts, member ts tss -> hlist typeDenote ts -> typeDenote t2)
529 -> typeDenote t2 :=
530 match tss return (forall ts, member ts tss -> option (hlist typeDenote ts))
531 -> (forall ts, member ts tss -> hlist typeDenote ts -> typeDenote t2)
532 -> _ with
533 | nil => fun _ _ =>
534 default
535 | ts :: tss' => fun (envs : forall ts', member ts' (ts :: tss')
536 -> option (hlist typeDenote ts'))
537 (bodies : forall ts', member ts' (ts :: tss')
538 -> hlist typeDenote ts' -> typeDenote t2) =>
539 match envs _ HFirst with
540 | None => matchesDenote
541 (fun _ mem => envs _ (HNext mem))
542 (fun _ mem => bodies _ (HNext mem))
543 | Some env => (bodies _ HFirst) env
544 end
545 end.
546 End matchesDenote.
547
548 Implicit Arguments matchesDenote [t2 tss].
549
550 Fixpoint expDenote t (e : exp typeDenote t) : typeDenote t :=
551 match e with
552 | Var _ v => v
553
554 | EUnit => tt
555
556 | App _ _ e1 e2 => (expDenote e1) (expDenote e2)
557 | Abs _ _ e' => fun x => expDenote (e' x)
558
559 | Pair _ _ e1 e2 => (expDenote e1, expDenote e2)
560
561 | EInl _ _ e' => inl _ (expDenote e')
562 | EInr _ _ e' => inr _ (expDenote e')
563
564 | Case _ _ _ e ps es def =>
565 matchesDenote (expDenote def)
566 (fun _ mem => patDenote (ps _ mem) (expDenote e))
567 (fun _ mem env => expDenote (es _ mem env))
568 end.
569
570 Definition ExpDenote t (E : Exp t) := expDenote (E _).
571 End Source.
572
573 Import Source.
574
575 Module Elab.
576 Section vars.
577 Variable var : type -> Type.
578
579 Inductive exp : type -> Type :=
580 | Var : forall t,
581 var t
582 -> exp t
583
584 | EUnit : exp Unit
585
586 | App : forall t1 t2,
587 exp (t1 --> t2)
588 -> exp t1
589 -> exp t2
590 | Abs : forall t1 t2,
591 (var t1 -> exp t2)
592 -> exp (t1 --> t2)
593
594 | Pair : forall t1 t2,
595 exp t1
596 -> exp t2
597 -> exp (t1 ** t2)
598 | Fst : forall t1 t2,
599 exp (t1 ** t2)
600 -> exp t1
601 | Snd : forall t1 t2,
602 exp (t1 ** t2)
603 -> exp t2
604
605 | EInl : forall t1 t2,
606 exp t1
607 -> exp (t1 ++ t2)
608 | EInr : forall t1 t2,
609 exp t2
610 -> exp (t1 ++ t2)
611 | Case : forall t1 t2 t,
612 exp (t1 ++ t2)
613 -> (var t1 -> exp t)
614 -> (var t2 -> exp t)
615 -> exp t.
616 End vars.
617
618 Definition Exp t := forall var, exp var t.
619
620 Implicit Arguments Var [var t].
621 Implicit Arguments EUnit [var].
622 Implicit Arguments App [var t1 t2].
623 Implicit Arguments Abs [var t1 t2].
624 Implicit Arguments Pair [var t1 t2].
625 Implicit Arguments Fst [var t1 t2].
626 Implicit Arguments Snd [var t1 t2].
627 Implicit Arguments EInl [var t1 t2].
628 Implicit Arguments EInr [var t1 t2].
629 Implicit Arguments Case [var t1 t2 t].
630
631
632 Notation "# v" := (Var v) (at level 70) : elab_scope.
633
634 Notation "()" := EUnit : elab_scope.
635
636 Infix "@" := App (left associativity, at level 77) : elab_scope.
637 Notation "\ x , e" := (Abs (fun x => e)) (at level 78) : elab_scope.
638 Notation "\ ? , e" := (Abs (fun _ => e)) (at level 78) : elab_scope.
639
640 Notation "[ x , y ]" := (Pair x y) : elab_scope.
641 Notation "#1 e" := (Fst e) (at level 72) : elab_scope.
642 Notation "#2 e" := (Snd e) (at level 72) : elab_scope.
643
644 Notation "'Inl' e" := (EInl e) (at level 71) : elab_scope.
645 Notation "'Inr' e" := (EInr e) (at level 71) : elab_scope.
646
647 Bind Scope elab_scope with exp.
648 Delimit Scope elab_scope with elab.
649
650 Open Scope elab_scope.
651
652 Fixpoint expDenote t (e : exp typeDenote t) : typeDenote t :=
653 match e with
654 | Var _ v => v
655
656 | EUnit => tt
657
658 | App _ _ e1 e2 => (expDenote e1) (expDenote e2)
659 | Abs _ _ e' => fun x => expDenote (e' x)
660
661 | Pair _ _ e1 e2 => (expDenote e1, expDenote e2)
662 | Fst _ _ e' => fst (expDenote e')
663 | Snd _ _ e' => snd (expDenote e')
664
665 | EInl _ _ e' => inl _ (expDenote e')
666 | EInr _ _ e' => inr _ (expDenote e')
667 | Case _ _ _ e' e1 e2 =>
668 match expDenote e' with
669 | inl v => expDenote (e1 v)
670 | inr v => expDenote (e2 v)
671 end
672 end.
673
674 Definition ExpDenote t (E : Exp t) := expDenote (E _).
675 End Elab.
676
677 Import Elab.
678
679 Notation "x <- e1 ; e2" := ((\x, e2) @ e1)%source
680 (right associativity, at level 76, e1 at next level) : source_scope.
681 Notation "x <- e1 ; e2" := ((\x, e2) @ e1)%elab
682 (right associativity, at level 76, e1 at next level) : elab_scope.
683
684 Section choice_tree.
685 Open Scope source_scope.
686
687 Fixpoint choice_tree var (t : type) (result : Type) : Type :=
688 match t with
689 | t1 ** t2 =>
690 choice_tree var t1
691 (choice_tree var t2
692 result)
693 | t1 ++ t2 =>
694 choice_tree var t1 result
695 * choice_tree var t2 result
696 | t => exp var t -> result
697 end%type.
698
699 Fixpoint merge var t result
700 : (result -> result -> result)
701 -> choice_tree var t result -> choice_tree var t result -> choice_tree var t result :=
702 match t with
703 | _ ** _ => fun mr ct1 ct2 =>
704 merge _ _
705 (merge _ _ mr)
706 ct1 ct2
707
708 | _ ++ _ => fun mr ct1 ct2 =>
709 (merge var _ mr (fst ct1) (fst ct2),
710 merge var _ mr (snd ct1) (snd ct2))
711
712 | _ => fun mr ct1 ct2 e => mr (ct1 e) (ct2 e)
713 end.
714
715 Fixpoint everywhere var t result
716 : (exp var t -> result) -> choice_tree var t result :=
717 match t with
718 | t1 ** t2 => fun r =>
719 everywhere (t := t1) (fun e1 =>
720 everywhere (t := t2) (fun e2 =>
721 r ([e1, e2])%elab))
722
723 | _ ++ _ => fun r =>
724 (everywhere (fun e => r (Inl e)%elab),
725 everywhere (fun e => r (Inr e)%elab))
726
727 | _ => fun r => r
728 end.
729 End choice_tree.
730
731 Implicit Arguments merge [var t result].
732
733 Section elaborate.
734 Local Open Scope elab_scope.
735
736 Fixpoint elaboratePat var t1 ts result (p : pat t1 ts) :
737 (hlist (exp var) ts -> result) -> result -> choice_tree var t1 result :=
738 match p with
739 | PVar _ => fun succ fail =>
740 everywhere (fun disc => succ (disc ::: HNil))
741
742 | PPair _ _ _ _ p1 p2 => fun succ fail =>
743 elaboratePat p1
744 (fun tup1 =>
745 elaboratePat p2
746 (fun tup2 =>
747 succ (happ tup1 tup2))
748 fail)
749 (everywhere (fun _ => fail))
750
751 | PInl _ _ _ p' => fun succ fail =>
752 (elaboratePat p' succ fail,
753 everywhere (fun _ => fail))
754 | PInr _ _ _ p' => fun succ fail =>
755 (everywhere (fun _ => fail),
756 elaboratePat p' succ fail)
757 end.
758
759 Implicit Arguments elaboratePat [var t1 ts result].
760
761 Fixpoint letify var t ts : (hlist var ts -> exp var t)
762 -> hlist (exp var) ts -> exp var t :=
763 match ts with
764 | nil => fun f _ => f HNil
765 | _ :: _ => fun f tup => letify (fun tup' => x <- hhd tup; f (x ::: tup')) (htl tup)
766 end.
767
768 Implicit Arguments letify [var t ts].
769
770 Fixpoint expand var result t1 t2
771 (out : result -> exp var t2)
772 : forall ct : choice_tree var t1 result,
773 exp var t1
774 -> exp var t2 :=
775 match t1 with
776 | (_ ** _)%source => fun ct disc =>
777 expand
778 (fun ct' => expand out ct' (#2 disc)%source)
779 ct
780 (#1 disc)
781
782 | (_ ++ _)%source => fun ct disc =>
783 Case disc
784 (fun x => expand out (fst ct) (#x))
785 (fun y => expand out (snd ct) (#y))
786
787 | _ => fun ct disc =>
788 x <- disc; out (ct (#x))
789 end.
790
791 Definition mergeOpt A (o1 o2 : option A) :=
792 match o1 with
793 | None => o2
794 | _ => o1
795 end.
796
797 Import Source.
798
799 Fixpoint elaborateMatches var t1 t2
800 (tss : list (list type))
801 : (forall ts, member ts tss -> pat t1 ts)
802 -> (forall ts, member ts tss -> hlist var ts -> Elab.exp var t2)
803 -> choice_tree var t1 (option (Elab.exp var t2)) :=
804 match tss return (forall ts, member ts tss -> pat t1 ts)
805 -> (forall ts, member ts tss -> hlist var ts -> Elab.exp var t2)
806 -> _ with
807 | nil => fun _ _ =>
808 everywhere (fun _ => None)
809 | ts :: tss' => fun (ps : forall ts', member ts' (ts :: tss') -> pat t1 ts')
810 (es : forall ts', member ts' (ts :: tss') -> hlist var ts' -> Elab.exp var t2) =>
811 merge (@mergeOpt _)
812 (elaboratePat (ps _ HFirst)
813 (fun ts => Some (letify
814 (fun ts' => es _ HFirst ts')
815 ts))
816 None)
817 (elaborateMatches
818 (fun _ mem => ps _ (HNext mem))
819 (fun _ mem => es _ (HNext mem)))
820 end.
821
822 Implicit Arguments elaborateMatches [var t1 t2 tss].
823
824 Open Scope cps_scope.
825
826 Fixpoint elaborate var t (e : Source.exp var t) : Elab.exp var t :=
827 match e with
828 | Var _ v => #v
829
830 | EUnit => ()
831
832 | App _ _ e1 e2 => elaborate e1 @ elaborate e2
833 | Abs _ _ e' => \x, elaborate (e' x)
834
835 | Pair _ _ e1 e2 => [elaborate e1, elaborate e2]
836 | EInl _ _ e' => Inl (elaborate e')
837 | EInr _ _ e' => Inr (elaborate e')
838
839 | Case _ _ _ e' ps es def =>
840 expand
841 (fun eo => match eo with
842 | None => elaborate def
843 | Some e => e
844 end)
845 (elaborateMatches ps (fun _ mem env => elaborate (es _ mem env)))
846 (elaborate e')
847 end.
848 End elaborate.
849
850 Definition Elaborate t (E : Source.Exp t) : Elab.Exp t :=
851 fun _ => elaborate (E _).
852
853 Fixpoint grab t result : choice_tree typeDenote t result -> typeDenote t -> result :=
854 match t with
855 | t1 ** t2 => fun ct v =>
856 grab t2 _ (grab t1 _ ct (fst v)) (snd v)
857 | t1 ++ t2 => fun ct v =>
858 match v with
859 | inl v' => grab t1 _ (fst ct) v'
860 | inr v' => grab t2 _ (snd ct) v'
861 end
862 | t => fun ct v => ct (#v)%elab
863 end%source%type.
864
865 Implicit Arguments grab [t result].
866
867 Ltac my_crush :=
868 crush;
869 repeat (match goal with
870 | [ |- context[match ?E with inl _ => _ | inr _ => _ end] ] =>
871 destruct E
872 end; crush).
873
874 Lemma expand_grab : forall t2 t1 result
875 (out : result -> Elab.exp typeDenote t2)
876 (ct : choice_tree typeDenote t1 result)
877 (disc : Elab.exp typeDenote t1),
878 Elab.expDenote (expand out ct disc)
879 = Elab.expDenote (out (grab ct (Elab.expDenote disc))).
880 induction t1; my_crush.
881 Qed.
882
883 Lemma recreate_pair : forall t1 t2
884 (x : Elab.exp typeDenote t1)
885 (x0 : Elab.exp typeDenote t2)
886 (v : typeDenote (t1 ** t2)),
887 expDenote x = fst v
888 -> expDenote x0 = snd v
889 -> @eq (typeDenote t1 * typeDenote t2) (expDenote [x, x0]) v.
890 destruct v; crush.
891 Qed.
892
893 Lemma everywhere_correct : forall t1 result
894 (succ : Elab.exp typeDenote t1 -> result) disc,
895 exists disc', grab (everywhere succ) (Elab.expDenote disc) = succ disc'
896 /\ Elab.expDenote disc' = Elab.expDenote disc.
897 Hint Resolve recreate_pair.
898
899 induction t1; my_crush; eauto; fold choice_tree;
900 repeat (fold typeDenote in *; crush;
901 match goal with
902 | [ IH : forall result succ, _ |- context[grab (everywhere ?S) _] ] =>
903 generalize (IH _ S); clear IH
904 | [ e : exp typeDenote (?T ** _), IH : forall _ : exp typeDenote ?T, _ |- _ ] =>
905 generalize (IH (#1 e)); clear IH
906 | [ e : exp typeDenote (_ ** ?T), IH : forall _ : exp typeDenote ?T, _ |- _ ] =>
907 generalize (IH (#2 e)); clear IH
908 | [ e : typeDenote ?T, IH : forall _ : exp typeDenote ?T, _ |- _ ] =>
909 generalize (IH (#e)); clear IH
910 end; crush); eauto.
911 Qed.
912
913 Lemma merge_correct : forall t result
914 (ct1 ct2 : choice_tree typeDenote t result)
915 (mr : result -> result -> result) v,
916 grab (merge mr ct1 ct2) v = mr (grab ct1 v) (grab ct2 v).
917 induction t; crush.
918 Qed.
919
920 Lemma everywhere_fail : forall t result
921 (fail : result) v,
922 grab (everywhere (fun _ : Elab.exp typeDenote t => fail)) v = fail.
923 induction t; crush.
924 Qed.
925
926 Lemma elaboratePat_correct : forall t1 ts (p : pat t1 ts)
927 result (succ : hlist (Elab.exp typeDenote) ts -> result)
928 (fail : result) v env,
929 patDenote p v = Some env
930 -> exists env', grab (elaboratePat p succ fail) v = succ env'
931 /\ env = hmap Elab.expDenote env'.
932 Hint Resolve hmap_happ.
933
934 induction p; crush; fold choice_tree;
935 repeat (match goal with
936 | [ |- context[grab (everywhere ?succ) ?v] ] =>
937 generalize (everywhere_correct succ (#v)%elab)
938
939 | [ H : forall result succ fail, _
940 |- context[grab (elaboratePat _ ?S ?F) ?V] ] =>
941 generalize (H _ S F V); clear H
942 | [ H1 : context[match ?E with Some _ => _ | None => _ end],
943 H2 : forall env, ?E = Some env -> _ |- _ ] =>
944 destruct E
945 | [ H : forall env, Some ?E = Some env -> _ |- _ ] =>
946 generalize (H _ (refl_equal _)); clear H
947 end; crush); eauto.
948 Qed.
949
950 Lemma elaboratePat_fails : forall t1 ts (p : pat t1 ts)
951 result (succ : hlist (Elab.exp typeDenote) ts -> result)
952 (fail : result) v,
953 patDenote p v = None
954 -> grab (elaboratePat p succ fail) v = fail.
955 Hint Resolve everywhere_fail.
956
957 induction p; try solve [ crush ];
958 simpl; fold choice_tree; intuition; simpl in *;
959 repeat match goal with
960 | [ IH : forall result succ fail v, patDenote ?P v = _ -> _
961 |- context[grab (elaboratePat ?P ?S ?F) ?V] ] =>
962 generalize (IH _ S F V); clear IH; intro IH;
963 generalize (elaboratePat_correct P S F V); intros;
964 destruct (patDenote P V); try discriminate
965 | [ H : forall env, Some _ = Some env -> _ |- _ ] =>
966 destruct (H _ (refl_equal _)); clear H; intuition
967 | [ H : _ |- _ ] => rewrite H; intuition
968 | [ |- context[match ?v with inl _ => _ | inr _ => _ end] ] =>
969 destruct v; auto
970 end.
971 Qed.
972
973 Implicit Arguments letify [var t ts].
974
975 Lemma letify_correct : forall t ts (f : hlist typeDenote ts -> Elab.exp typeDenote t)
976 (env : hlist (Elab.exp typeDenote) ts),
977 Elab.expDenote (letify f env)
978 = Elab.expDenote (f (hmap Elab.expDenote env)).
979 induction ts; crush; dep_destruct env; crush.
980 Qed.
981
982 Theorem elaborate_correct : forall t (e : Source.exp typeDenote t),
983 Elab.expDenote (elaborate e) = Source.expDenote e.
984 Hint Rewrite expand_grab merge_correct letify_correct : cpdt.
985 Hint Rewrite everywhere_fail elaboratePat_fails using assumption : cpdt.
986
987 induction e; crush; try (ext_eq; crush);
988 match goal with
989 | [ tss : list (list type) |- _ ] =>
990 induction tss; crush;
991 match goal with
992 | [ |- context[grab (elaboratePat ?P ?S ?F) ?V] ] =>
993 case_eq (patDenote P V); [intros env Heq;
994 destruct (elaboratePat_correct P S F _ Heq); crush;
995 match goal with
996 | [ H : _ |- _ ] => rewrite <- H; crush
997 end
998 | crush ]
999 end
1000 end.
1001 Qed.
1002
1003 Theorem Elaborate_correct : forall t (E : Source.Exp t),
1004 Elab.ExpDenote (Elaborate E) = Source.ExpDenote E.
1005 unfold Elab.ExpDenote, Elaborate, Source.ExpDenote;
1006 intros; apply elaborate_correct.
1007 Qed.
1008
1009 End PatMatch.
1010
1011
1012 (** * Exercises *) 387 (** * Exercises *)
1013 388
1014 (** %\begin{enumerate}%#<ol># 389 (** %\begin{enumerate}%#<ol>#
1015 390
1016 %\item%#<li># When in the last chapter we implemented constant folding for simply-typed lambda calculus, it may have seemed natural to try applying beta reductions. This would have been a lot more trouble than is apparent at first, because we would have needed to convince Coq that our normalizing function always terminated. 391 %\item%#<li># When in the last chapter we implemented constant folding for simply-typed lambda calculus, it may have seemed natural to try applying beta reductions. This would have been a lot more trouble than is apparent at first, because we would have needed to convince Coq that our normalizing function always terminated.