for @{ 'leaf_ko $a $t }.
interpretation "leaf KO" 'leaf_ko a t = (cast _ _ (show a t)).
-(* already proved lemma *)
-definition Lemma : ΠA.A→A ≝ λA:CProp.λa:A.a.
-
-notation < "\infrule \nbsp p mstyle color #ff0000 (\lem\emsp H)" non associative with precedence 19
-for @{ 'lemma_ko_1 $p $H }.
-interpretation "lemma_ko_1" 'lemma_ko_1 p H =
- (show p (cast _ _ (Lemma _ H))).
-
-notation < "\infrule \nbsp mstyle color #ff0000 (p) mstyle color #ff0000 (\lem\emsp H)" non associative with precedence 19
-for @{ 'lemma_ko_2 $p $H }.
-interpretation "lemma_ko_2" 'lemma_ko_2 p H =
- (cast _ _ (show p (cast _ _ (Lemma _ H)))).
-
-notation < "\infrule \nbsp p (\lem\emsp H)" non associative with precedence 19
-for @{ 'lemma_ok_1 $p $H }.
-interpretation "lemma_ok_1" 'lemma_ok_1 p H =
- (show p (Lemma _ H)).
-interpretation "lemma_ok_11" 'lemma_ok_1 p H =
- (show p (Lemma _ H _)).
-interpretation "lemma_ok_111" 'lemma_ok_1 p H =
- (show p (Lemma _ H _ _)).
-
-notation < "\infrule \nbsp mstyle color #ff0000 (p) (\lem\emsp H)" non associative with precedence 19
-for @{ 'lemma_ok_2 $p $H }.
-interpretation "lemma_ok_2" 'lemma_ok_2 p H =
- (cast _ _ (show p (Lemma _ H))).
-interpretation "lemma_ok_22" 'lemma_ok_2 p H =
- (cast _ _ (show p (Lemma _ H _))).
-interpretation "lemma_ok_22" 'lemma_ok_2 p H =
- (cast _ _ (show p (Lemma _ H _ _))).
-
-notation > "'lem' term 90 p" non associative with precedence 19
-for @{ 'Lemma $p }.
-interpretation "lemma KO" 'Lemma p = (cast _ _ (Lemma _ p)).
-interpretation "lemma OK" 'Lemma p = (Lemma _ p).
-
-
(* discharging *)
notation < "[ a ] \sup mstyle color #ff0000 (H)" with precedence 19
for @{ 'discharge_ko_1 $a $H }.
(cast _ unit (Forall_elim sort P t (cast _ _ Px))).
interpretation "Forall_elim OK" 'Forall_elim P t Px =
(Forall_elim sort P t Px).
+
+(* already proved lemma *)
+definition hide_args : ∀A:Type.∀a:A.A := λA:Type.λa:A.a.
+notation < "t" non associative with precedence 90 for @{'hide_args $t}.
+interpretation "hide 0 args" 'hide_args t = (hide_args _ t).
+interpretation "hide 1 args" 'hide_args t = (hide_args _ t _).
+interpretation "hide 2 args" 'hide_args t = (hide_args _ t _ _).
+interpretation "hide 3 args" 'hide_args t = (hide_args _ t _ _ _).
+interpretation "hide 4 args" 'hide_args t = (hide_args _ t _ _ _ _).
+interpretation "hide 5 args" 'hide_args t = (hide_args _ t _ _ _ _ _).
+interpretation "hide 6 args" 'hide_args t = (hide_args _ t _ _ _ _ _ _).
+interpretation "hide 7 args" 'hide_args t = (hide_args _ t _ _ _ _ _ _ _).
+
+(* more args crashes the pattern matcher *)
+
+(* already proved lemma, 0 assumptions *)
+definition Lemma : ΠA.A→A ≝ λA:CProp.λa:A.a.
+
+notation < "\infrule
+ (\infrule
+ (\emsp)
+ (╲ mstyle mathsize normal (mstyle color #ff0000 (H)) ╱) \nbsp)
+ p \nbsp"
+non associative with precedence 19
+for @{ 'lemma_ko_1 $p ($H : $_) }.
+interpretation "lemma_ko_1" 'lemma_ko_1 p H =
+ (show p (cast _ _ (Lemma _ (cast _ _ H)))).
+
+notation < "\infrule
+ (\infrule
+ (\emsp)
+ (╲ mstyle mathsize normal (mstyle color #ff0000 (H)) ╱) \nbsp)
+ mstyle color #ff0000 (p) \nbsp"
+non associative with precedence 19
+for @{ 'lemma_ko_2 $p ($H : $_) }.
+interpretation "lemma_ko_2" 'lemma_ko_2 p H =
+ (cast _ _ (show p (cast _ _
+ (Lemma _ (cast _ _ H))))).
+
+
+notation < "\infrule
+ (\infrule
+ (\emsp)
+ (╲ mstyle mathsize normal (H) ╱) \nbsp)
+ p \nbsp"
+non associative with precedence 19
+for @{ 'lemma_ok_1 $p ($H : $_) }.
+interpretation "lemma_ok_1" 'lemma_ok_1 p H =
+ (show p (Lemma _ H)).
+
+notation < "\infrule
+ (\infrule
+ (\emsp)
+ (╲ mstyle mathsize normal (H) ╱) \nbsp)
+ mstyle color #ff0000 (p) \nbsp"
+non associative with precedence 19
+for @{ 'lemma_ok_2 $p ($H : $_) }.
+interpretation "lemma_ok_2" 'lemma_ok_2 p H =
+ (cast _ _ (show p (Lemma _ H))).
+
+notation > "'lem' 0 term 90 l" non associative with precedence 19
+for @{ 'Lemma (hide_args ? $l : ?) }.
+interpretation "lemma KO" 'Lemma l =
+ (cast _ _ (Lemma unit (cast unit _ l))).
+interpretation "lemma OK" 'Lemma l = (Lemma _ l).
+
+
+(* already proved lemma, 1 assumption *)
+definition Lemma1 : ΠA,B. (A ⇒ B) → A → B ≝
+ λA,B:CProp.λf:A⇒B.λa:A.
+ Imply_elim A B f a.
+
+notation < "\infrule
+ (\infrule
+ (\emsp a \emsp)
+ (╲ mstyle mathsize normal (mstyle color #ff0000 (H)) ╱) \nbsp)
+ p \nbsp"
+non associative with precedence 19
+for @{ 'lemma1_ko_1 $a $p ($H : $_) }.
+interpretation "lemma1_ko_1" 'lemma1_ko_1 a p H =
+ (show p (cast _ _ (Lemma1 _ _ (cast _ _ H) (cast _ _ a)))).
+
+notation < "\infrule
+ (\infrule
+ (\emsp a \emsp)
+ (╲ mstyle mathsize normal (mstyle color #ff0000 (H)) ╱) \nbsp)
+ mstyle color #ff0000 (p) \nbsp"
+non associative with precedence 19
+for @{ 'lemma1_ko_2 $a $p ($H : $_) }.
+interpretation "lemma1_ko_2" 'lemma1_ko_2 a p H =
+ (cast _ _ (show p (cast _ _
+ (Lemma1 _ _ (cast _ _ H) (cast _ _ a))))).
+
+
+notation < "\infrule
+ (\infrule
+ (\emsp a \emsp)
+ (╲ mstyle mathsize normal (H) ╱) \nbsp)
+ p \nbsp"
+non associative with precedence 19
+for @{ 'lemma1_ok_1 $a $p ($H : $_) }.
+interpretation "lemma1_ok_1" 'lemma1_ok_1 a p H =
+ (show p (Lemma1 _ _ H a)).
+
+notation < "\infrule
+ (\infrule
+ (\emsp a \emsp)
+ (╲ mstyle mathsize normal (H) ╱) \nbsp)
+ mstyle color #ff0000 (p) \nbsp"
+non associative with precedence 19
+for @{ 'lemma1_ok_2 $a $p ($H : $_) }.
+interpretation "lemma1_ok_2" 'lemma1_ok_2 a p H =
+ (cast _ _ (show p (Lemma1 _ _ H a))).
+
+
+notation > "'lem' 1 term 90 l term 90 p" non associative with precedence 19
+for @{ 'Lemma1 (hide_args ? $l : ?) (show $p ?) }.
+interpretation "lemma 1 KO" 'Lemma1 l p =
+ (cast _ _ (Lemma1 unit unit (cast (Imply unit unit) _ l) (cast unit _ p))).
+interpretation "lemma 1 OK" 'Lemma1 l p = (Lemma1 _ _ l p).
+
+(* already proved lemma, 2 assumptions *)
+definition Lemma2 : ΠA,B,C. (A ⇒ B ⇒ C) → A → B → C ≝
+ λA,B,C:CProp.λf:A⇒B⇒C.λa:A.λb:B.
+ Imply_elim B C (Imply_elim A (B⇒C) f a) b.
+
+notation < "\infrule
+ (\infrule
+ (\emsp a \emsp\emsp\emsp b \emsp)
+ (╲ mstyle mathsize normal (mstyle color #ff0000 (H)) ╱) \nbsp)
+ p \nbsp"
+non associative with precedence 19
+for @{ 'lemma2_ko_1 $a $b $p ($H : $_) }.
+interpretation "lemma2_ko_1" 'lemma2_ko_1 a b p H =
+ (show p (cast _ _ (Lemma2 _ _ _ (cast _ _ H) (cast _ _ a) (cast _ _ b)))).
+
+notation < "\infrule
+ (\infrule
+ (\emsp a \emsp\emsp\emsp b \emsp)
+ (╲ mstyle mathsize normal (mstyle color #ff0000 (H)) ╱) \nbsp)
+ mstyle color #ff0000 (p) \nbsp"
+non associative with precedence 19
+for @{ 'lemma2_ko_2 $a $b $p ($H : $_) }.
+interpretation "lemma2_ko_2" 'lemma2_ko_2 a b p H =
+ (cast _ _ (show p (cast _ _
+ (Lemma2 _ _ _ (cast _ _ H) (cast _ _ a) (cast _ _ b))))).
+
+
+notation < "\infrule
+ (\infrule
+ (\emsp a \emsp\emsp\emsp b \emsp)
+ (╲ mstyle mathsize normal (H) ╱) \nbsp)
+ p \nbsp"
+non associative with precedence 19
+for @{ 'lemma2_ok_1 $a $b $p ($H : $_) }.
+interpretation "lemma2_ok_1" 'lemma2_ok_1 a b p H =
+ (show p (Lemma2 _ _ _ H a b)).
+
+notation < "\infrule
+ (\infrule
+ (\emsp a \emsp\emsp\emsp b \emsp)
+ (╲ mstyle mathsize normal (H) ╱) \nbsp)
+ mstyle color #ff0000 (p) \nbsp"
+non associative with precedence 19
+for @{ 'lemma2_ok_2 $a $b $p ($H : $_) }.
+interpretation "lemma2_ok_2" 'lemma2_ok_2 a b p H =
+ (cast _ _ (show p (Lemma2 _ _ _ H a b))).
+
+notation > "'lem' 2 term 90 l term 90 p term 90 q" non associative with precedence 19
+for @{ 'Lemma2 (hide_args ? $l : ?) (show $p ?) (show $q ?) }.
+interpretation "lemma 2 KO" 'Lemma2 l p q =
+ (cast _ _ (Lemma2 unit unit unit (cast (Imply unit (Imply unit unit)) _ l) (cast unit _ p) (cast unit _ q))).
+interpretation "lemma 2 OK" 'Lemma2 l p q = (Lemma2 _ _ _ l p q).
+
+(* already proved lemma, 3 assumptions *)
+definition Lemma3 : ΠA,B,C,D. (A ⇒ B ⇒ C ⇒ D) → A → B → C → D ≝
+ λA,B,C,D:CProp.λf:A⇒B⇒C⇒D.λa:A.λb:B.λc:C.
+ Imply_elim C D (Imply_elim B (C⇒D) (Imply_elim A (B⇒C⇒D) f a) b) c.
+
+notation < "\infrule
+ (\infrule
+ (\emsp a \emsp\emsp\emsp b \emsp\emsp\emsp c \emsp)
+ (╲ mstyle mathsize normal (mstyle color #ff0000 (H)) ╱) \nbsp)
+ p \nbsp"
+non associative with precedence 19
+for @{ 'lemma3_ko_1 $a $b $c $p ($H : $_) }.
+interpretation "lemma3_ko_1" 'lemma3_ko_1 a b c p H =
+ (show p (cast _ _
+ (Lemma3 _ _ _ _ (cast _ _ H) (cast _ _ a) (cast _ _ b) (cast _ _ c)))).
+
+notation < "\infrule
+ (\infrule
+ (\emsp a \emsp\emsp\emsp b \emsp\emsp\emsp c \emsp)
+ (╲ mstyle mathsize normal (mstyle color #ff0000 (H)) ╱) \nbsp)
+ mstyle color #ff0000 (p) \nbsp"
+non associative with precedence 19
+for @{ 'lemma3_ko_2 $a $b $c $p ($H : $_) }.
+interpretation "lemma3_ko_2" 'lemma3_ko_2 a b c p H =
+ (cast _ _ (show p (cast _ _
+ (Lemma3 _ _ _ _ (cast _ _ H) (cast _ _ a) (cast _ _ b) (cast _ _ c))))).
+
+
+notation < "\infrule
+ (\infrule
+ (\emsp a \emsp\emsp\emsp b \emsp\emsp\emsp c \emsp)
+ (╲ mstyle mathsize normal (H) ╱) \nbsp)
+ p \nbsp"
+non associative with precedence 19
+for @{ 'lemma3_ok_1 $a $b $c $p ($H : $_) }.
+interpretation "lemma3_ok_1" 'lemma3_ok_1 a b c p H =
+ (show p (Lemma3 _ _ _ _ H a b c)).
+
+notation < "\infrule
+ (\infrule
+ (\emsp a \emsp\emsp\emsp b \emsp\emsp\emsp c \emsp)
+ (╲ mstyle mathsize normal (H) ╱) \nbsp)
+ mstyle color #ff0000 (p) \nbsp"
+non associative with precedence 19
+for @{ 'lemma3_ok_2 $a $b $c $p ($H : $_) }.
+interpretation "lemma3_ok_2" 'lemma3_ok_2 a b c p H =
+ (cast _ _ (show p (Lemma3 _ _ _ _ H a b c))).
+
+notation > "'lem' 3 term 90 l term 90 p term 90 q term 90 r" non associative with precedence 19
+for @{ 'Lemma3 (hide_args ? $l : ?) (show $p ?) (show $q ?) (show $r ?) }.
+interpretation "lemma 3 KO" 'Lemma3 l p q r =
+ (cast _ _ (Lemma3 unit unit unit unit (cast (Imply unit (Imply unit (Imply unit unit))) _ l) (cast unit _ p) (cast unit _ q) (cast unit _ r))).
+interpretation "lemma 3 OK" 'Lemma3 l p q r = (Lemma3 _ _ _ _ l p q r).
projects / helm.git / blobdiff