aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--scratch.thy9
-rw-r--r--tests/Schematic_subgoal.thy64
2 files changed, 64 insertions, 9 deletions
diff --git a/scratch.thy b/scratch.thy
deleted file mode 100644
index f0514c3..0000000
--- a/scratch.thy
+++ /dev/null
@@ -1,9 +0,0 @@
-theory scratch
- imports HoTT
-begin
-
-
-
-
-
-end \ No newline at end of file
diff --git a/tests/Schematic_subgoal.thy b/tests/Schematic_subgoal.thy
new file mode 100644
index 0000000..5f20eac
--- /dev/null
+++ b/tests/Schematic_subgoal.thy
@@ -0,0 +1,64 @@
+theory Schematic_subgoal
+ imports "../HoTT"
+begin
+
+text "
+ \<open>subgoal\<close> converts schematic variables to fixed free variables, making it unsuitable for use in \<open>schematic_goal\<close> proofs.
+
+ This is a problem for syntheses which need to use induction (elimination rules), as these often have to be applied to fixed variables, while keeping any schematic variables intact.
+"
+
+schematic_goal rpathcomp_synthesis:
+ assumes "A: U(i)"
+ shows "?a: \<Prod>x:A. \<Prod>y:A. x =\<^sub>A y \<rightarrow> (\<Prod>z:A. y =\<^sub>A z \<rightarrow> x =\<^sub>A z)"
+
+text "
+ Try (and fail) to synthesize the constant for path composition, following the proof of \<open>rpathcomp_type\<close> below.
+"
+
+apply (rule Prod_intro)
+prefer 2
+ apply (rule Prod_intro)
+ prefer 2
+ apply (rule Prod_intro)
+ prefer 2
+ subgoal 123 for x y p
+ apply (rule Equal_elim[where ?x=x and ?y=y and ?A=A])
+ oops
+
+
+lemma rpathcomp_type:
+ assumes "A: U(i)"
+ shows "rpathcomp: \<Prod>x:A. \<Prod>y:A. x =\<^sub>A y \<rightarrow> (\<Prod>z:A. y =\<^sub>A z \<rightarrow> x =\<^sub>A z)"
+unfolding rpathcomp_def
+apply standard
+prefer 2
+ subgoal premises 1 for x \<comment> \<open>\<open>subgoal\<close> is the proof script version of \<open>fix-assume-show\<close>.\<close>
+ apply standard
+ prefer 2
+ subgoal premises 2 for y
+ apply standard
+ prefer 2
+ subgoal premises 3 for p
+ apply (rule Equal_elim[where ?x=x and ?y=y and ?A=A])
+ \<comment> \<open>specifying \<open>?A=A\<close> is crucial here to prevent the next \<open>subgoal\<close> from binding a schematic ?A which should be instantiated to \<open>A\<close>.\<close>
+ prefer 2
+ apply standard
+ prefer 2
+ apply (rule Prod_intro)
+ prefer 2
+ subgoal premises 4 for u z q
+ apply (rule Equal_elim[where ?x=u and ?y=z])
+ apply (simple lems: assms 4)
+ done
+ apply (simple lems: assms 1 2 3)
+ done
+ apply (simple lems: assms 1 2)
+ done
+ apply fact
+ done
+apply fact
+done
+
+
+end \ No newline at end of file