Chasing admits

examples/Vector_tuple.v

@@ -311,28 +311,12 @@ Definition bv_to_nat : forall {k : nat}, bitvector k -> nat :=
       (match b with true => S | false => id end) (2 * F k' bv')%nat
     end.
 
-Lemma S_add1 : forall (n : nat), S n = (n + 1)%nat.
-Proof.
-  induction n.
-  - simpl. reflexivity.
-  - by rewrite addn1.
-Defined.
-
-Lemma one_lt_pow2 (k : nat) : (1 <= expn 2 k)%nat = true.
-Proof.
-Search expn (leq 1).
-  induction k.
-  - simpl.
-Admitted.
-
-Axiom bv_bound :
-  forall {k : nat} (bv : bitvector k), (bv_to_nat bv <= expn 2 k - 1)%nat = true.
-
 Definition bv_to_bnat {k : nat} (bv : bitvector k) : bounded_nat k.
 Proof.
   unshelve econstructor.
   - exact (bv_to_nat bv).
-Admitted.
+  - by rewrite ltn_expl.
+Qed.
 
 Axiom map_in_R_bv_bnat :
   forall {k : nat} {bv : bitvector k} {bn : bounded_nat k},

examples/int_to_Zp.v

@@ -17,22 +17,22 @@ Import GRing.Theory.
 Local Open Scope bool_scope.
 
 Set Universe Polymorphism.
-
-Lemma val_Zp_int p : 1 < p ->
-  forall n : int, ((n%:~R)%R : 'Z_p)%:Z%R = (n %% p)%Z.
-Proof.
-case: p => [|[|p]]// _ [] n /=.
-  by rewrite modz_nat -val_Zp_nat.
-rewrite modNz_nat// val_Zp_nat//= /Zp_trunc/=.
-rewrite modnS.
-case: ifP.
-  rewrite subn0 modnn.
-Admitted.
 
 Lemma Zp_int_mod [p : nat] : 1 < p ->
-   forall m : int, ((m %% p)%Z%:~R)%R = (m%:~R)%R :> 'Z_p.
-Admitted.
+   forall n : int, ((n %% p)%Z%:~R)%R = (n%:~R)%R :> 'Z_p.
+Proof.
+move=> p_gt1 n; rewrite [in RHS](divz_eq n p) [in RHS]intrD intrM.
+by rewrite [p%:~R%R]char_Zp// mulr0 add0r.
+Qed.
 
+Lemma val_Zp_int p : 1 < p ->
+  forall n : int, ((n%:~R)%R : 'Z_p)%:Z%R = (n %% p)%Z.
+Proof.
+move=> p_gt1 n; rewrite -Zp_int_mod//.
+have: ((n %% p)%Z >= 0)%R by rewrite modz_ge0//; case: p p_gt1.
+rewrite -[RHS]modz_mod; case: (n %% p)%Z => //= k _ /=.
+by rewrite val_Zp_nat// modz_nat.
+Qed.
 
 Section modp.
 Variable (p : nat) (p_gt1 : p > 1).

theories/Common.v

@@ -146,7 +146,7 @@ Let map_in_comap b a (e : f a = b) : comap f b = a :=
 
 Let map_in_comapK b a (e : f a = b) :
   comap_in_map b a (map_in_comap b a e) = e.
-Proof. Admitted.
+Proof. exact: Prop_irrelevance. Qed.
 
 Definition toParam@{} : Param44.Rel@{i} A B :=
   @Param44.BuildRel A B (graph f)

theories/Hierarchy.v

@@ -357,6 +357,101 @@ Notation MkUMap := Map4.BuildHas.
 Arguments Map4.BuildHas {A B R}.
 Arguments Param44.BuildRel {A B R}.
 
+(* General theorems *)
+Lemma ind_map@{i} {A A' : Type@{i}} (AR : Param40.Rel@{i} A A') a
+  (P : forall a', AR a a' -> map AR a = a' -> Type@{i}) :
+  (P (map AR a) (map_in_R AR a (map AR a) 1%path) 1%path) ->
+  forall a' aR, P a' aR (R_in_map AR a a' aR).
+Proof.
+by move=> P1 a' aR; rewrite -[X in P _ X](R_in_mapK AR); case: _ / R_in_map.
+Defined.
+
+Lemma ind_mapP@{i +} {A A' : Type@{i}} (AR : Param40.Rel@{i} A A') (a : A)
+  (P : forall a', AR a a' -> map@{i} AR a = a' -> Type@{i})
+  (P1 : P (map@{i} AR a) (map_in_R@{i} AR a (map@{i} AR a) 1%path) 1%path)
+  (Q : forall a' aR e, P a' aR e -> Type@{i}) :
+   Q (map@{i} AR a) (map_in_R@{i} AR a (map@{i} AR a) 1%path) 1%path P1 ->
+  forall a' aR,
+     Q a' aR (R_in_map@{i} AR a a' aR) (@ind_map@{i} A A' AR a P P1 a' aR).
+Proof.
+rewrite /ind_map => Q1 a' aR.
+case: {1 6}_ / R_in_mapK.
+by case: _ / R_in_map.
+Qed.
+
+Lemma weak_ind_map@{i} {A A' : Type@{i}} (AR : Param40.Rel@{i} A A') a
+  (P : forall a', AR a a' -> Type@{i}) :
+  (P (map AR a) (map_in_R AR a (map AR a) 1%path)) ->
+  forall a' aR, P a' aR.
+Proof. by move=> P1 a' aR; elim/(ind_map AR): aR / _. Defined.
+
+Lemma ind_comap@{i} {A A' : Type@{i}} (AR : Param04.Rel@{i} A A') a'
+  (P : forall a, AR a a' -> comap AR a' = a -> Type@{i}) :
+  (P (comap AR a') (comap_in_R AR a' (comap AR a') 1%path) 1%path) ->
+  forall a aR, P a aR (R_in_comap AR a' a aR).
+Proof.
+by move=> P1 a aR; rewrite -[X in P _ X](R_in_comapK AR); case: _ / R_in_comap.
+Defined.
+
+Lemma ind_comapP@{i +} {A A' : Type@{i}} (AR : Param04.Rel@{i} A A') a'
+  (P : forall a, AR a a' -> comap AR a' = a -> Type@{i})
+  (P1 : P (comap@{i} AR a') (comap_in_R@{i} AR a' (comap@{i} AR a') 1%path) 1%path)
+  (Q : forall a aR e, P a aR e -> Type@{i}) :
+   Q (comap@{i} AR a') (comap_in_R@{i} AR a' (comap@{i} AR a') 1%path) 1%path P1 ->
+  forall a aR,
+     Q a aR (R_in_comap@{i} AR a' a aR) (@ind_comap@{i} A A' AR a' P P1 a aR).
+Proof.
+rewrite /ind_comap => Q1 a aR.
+case: {1 6}_ / R_in_comapK.
+by case: _ / R_in_comap.
+Qed.
+
+Lemma weak_ind_comap@{i} {A A' : Type@{i}} (AR : Param04.Rel@{i} A A') a'
+  (P : forall a, AR a a' -> Type@{i}) :
+  (P (comap AR a') (comap_in_R AR a' (comap AR a') 1%path)) ->
+  forall a aR, P a aR. 
+Proof. by move=> P1 a aR; elim/(ind_comap AR): aR / _. Defined.
+
+Definition map_ind@{i} {A A' : Type@{i}} {PA : Param40.Rel@{i} A A'}
+    (a : A) (a' : A') (aR : PA a a')
+    (P : forall (a' : A'), PA a a' -> Type@{i})  :
+   P a' aR -> P (map PA a) (map_in_R PA a (map PA a) idpath).
+Proof. by elim/(ind_map PA): _ aR / _. Defined.
+(* 
+
+apply (transport
+  (fun aR0 : PA a a' =>
+    P a' aR0 -> P (map PA a)
+                 (map_in_R PA a (map PA a) idpath))
+  (R_in_mapK PA a a' aR)
+  (paths_rect A' (map PA a)
+  (fun (a0 : A') (e : map PA a = a0) =>
+   P a0 (map_in_R PA a a0 e) ->
+   P (map PA a)
+    (map_in_R PA a (map PA a) idpath)) idmap a'
+  (R_in_map PA a a' aR))).
+Defined. *)
+
+Definition comap_ind@{i} {A A' : Type@{i}} {PA : Param04.Rel@{i} A A'}
+    (a : A) (a' : A') (aR : PA a a')
+    (P : forall (a : A), PA a a' -> Type@{i})  :
+   P a aR -> P (comap PA a') (comap_in_R PA a' (comap PA a') idpath).
+Proof. by elim/(ind_comap PA): _ aR / _. Defined.
+(* Proof.
+apply (transport
+  (fun aR0 : PA a a' =>
+    P a aR0 -> P (comap PA a')
+                 (comap_in_R PA a' (comap PA a') idpath))
+  (R_in_comapK PA a' a aR)
+  (paths_rect A (comap PA a')
+  (fun (a0 : A) (e : comap PA a' = a0) =>
+   P a0 (comap_in_R PA a' a0 e) ->
+   P (comap PA a')
+    (comap_in_R PA a' (comap PA a') idpath)) idmap a
+  (R_in_comap PA a' a aR))).
+Defined. *)
+
+
 (* symmetry lemmas for Map *)
 
 Definition eq_Map0w@{i} {A A' : Type@{i}} {R R' : A -> A' -> Type@{i}} :
@@ -440,25 +535,6 @@ move=> RR' [m mR Rm RmK]; unshelve eexists m _ _.
   by case: RR' => /= f [/= g ].
 Defined.
 
-(* joined elimination of comap and comap_in_R *)
-
-Definition comap_ind@{i j} {A A' : Type@{i}} {PA : Param04.Rel A A'}
-    (a : A) (a' : A') (aR : PA a a')
-    (P : forall (a : A), PA a a' -> Type@{j})  :
-   P a aR -> P (comap PA a') (comap_in_R PA a' (comap PA a') idpath).
-Proof.
-apply (transport
-  (fun aR0 : PA a a' =>
-    P a aR0 -> P (comap PA a')
-                 (comap_in_R PA a' (comap PA a') idpath))
-  (R_in_comapK PA a' a aR)
-  (paths_rect A (comap PA a')
-  (fun (a0 : A) (e : comap PA a' = a0) =>
-   P a0 (comap_in_R PA a' a0 e) ->
-   P (comap PA a')
-    (comap_in_R PA a' (comap PA a') idpath)) idmap a
-  (R_in_comap PA a' a aR))).
-Defined.
 
 Definition id_umap@{i} {A : Type@{i}} : IsUMap (@paths A) :=
   MkUMap idmap (fun a b r => r) (fun a b r => r) (fun a b r => 1%path).

theories/Param_arrow.v

@@ -103,8 +103,14 @@ Proof.
   apply path_forall@{i k} => a.
   apply path_forall@{i k} => a'.
   apply path_arrow@{i k} => aR /=.
-  rewrite -[in X in _ = X](R_in_comapK PA a' a aR).
-Admitted.
+  elim/(ind_comap PA): _ => {a aR}.
+  rewrite transport1.
+  set X := transport _ _ _.
+  have -> : X = R_in_map PB (f (comap PA a')) (f' a') (fR (comap PA a') a'
+    (comap_in_R PA a' (comap PA a') 1)).
+    exact: Prop_irrelevance.
+  by elim/(ind_map PB): _ (fR _ _ _) / _.
+  Qed.
 
 (* Param_arrowMN : forall A A' AR B B' BR, ParamMN.Rel (A -> B) (A' -> B') *)
 

theories/Param_forall.v

@@ -94,9 +94,9 @@ Definition Map2a_forall@{i j k}
     Map2a.Has@{k} (R_forall@{i j} PA PB).
 Proof.
   exists (Map1.map@{k} _ (Map1_forall@{i j k} PA PB)).
-  move=> f f' e a a' aR; apply (map_in_R@{j} (PB _ _ _)).
-  apply (transport@{j j} (fun t => _ = t a') e) => /=.
-  by elim/(comap_ind@{i j} a a' aR): _.
+  move=> f f' /= e a a' aR; apply (map_in_R@{j} (PB _ _ _)).
+  elim/(ind_comap PA): _ aR / _.
+  exact: (ap (fun f => f a') e).
 Defined.
 
 (* (02a, 2b0) + funext -> 2b0 *)
@@ -124,6 +124,10 @@ Proof.
     apply (R_in_map (PB _ _ _)); exact: fR.
 Defined.
 
+Lemma ap_path_forall `{Funext} X Y (f g : forall x : X, Y x) x (e : f == g):
+  ap (fun f => f x) (path_forall f g e) = e x.
+Proof. exact: Prop_irrelevance. Qed.
+
 (* (04, 40) + funext -> 40 *)
 Definition Map4_forall@{i j k} `{Funext}
   {A A' : Type@{i}} (PA : Param04.Rel@{i} A A')
@@ -139,14 +143,10 @@ Proof.
   apply path_forall@{i k} => a.
   apply path_forall@{i k} => a'.
   apply path_forall => aR.
-  unfold comap_ind.
-  elim (R_in_comapK PA a' a aR) => /=.
-  (* elim (R_in_comap PA a' a aR).
-  rewrite transport_apD10.
-  rewrite apD10_path_forall_cancel/=.
-  rewrite <- (R_in_mapK (PB _ _ _)).
-  by elim: (R_in_map _ _ _ _). *)
-Admitted.
+  elim/(ind_comapP PA): _ => {a aR}.
+  rewrite ap_path_forall.
+  by elim/(ind_map (PB (comap PA a') a' (comap_in_R PA a' (comap PA a') 1))): _ _ / _.
+ Qed.
 (* Param_forallMN : forall A A' AR B B' BR,
      ParamMN.Rel (forall a, B a) (forall a', B' a') *)
 

theories/Param_nat.v

@@ -21,6 +21,26 @@ Inductive natR : nat -> nat -> Type :=
   | OR : natR O O
   | SR : forall (n n' : nat), natR n n' -> natR (S n) (S n').
 
+Lemma ind (T : Type) (X : T -> Type) t (P : X t -> Type) :
+  (forall t' (e : t' = t) (x : X t'), P (transport X e x)) ->
+  forall (x : X t), P x.
+Proof. by move=> + x => /(_ t erefl); apply. Defined.
+
+Lemma eq_to_refl (T : Type) (x : T) (p : x = x) : unkeyed p = erefl.
+Proof. exact: Prop_irrelevance. Qed.
+
+Lemma natR_irrelevant m n : forall (nR nR' : natR m n), nR = nR'.
+Proof.
+suff: forall (nR : natR m n) m' n'  (nR' : natR m' n') (e : m = m') (e' : n = n') ,
+     transport (fun m' => natR m' n') e (transport (fun n' => natR m n') e' nR) = nR'.
+    by move=> /(_ _ m n _ erefl erefl); apply.
+elim => // [|{}m {}n nR IHnR] m' n' => - [|{}m' {}n' nR'] // e e'.
+  by rewrite ?eq_to_refl.
+rewrite -[nR']IHnR//; do ?by [case: e|case: e'].
+move=> e'' e'''.
+by case: _ / e'' in e *; case: _ / e''' in e' *; rewrite ?eq_to_refl.
+Qed.
+
 Definition map_nat : nat -> nat := id.
 
 Definition map_in_R_nat : forall {n n' : nat}, map_nat n = n' -> natR n n' :=
@@ -43,7 +63,9 @@ Definition R_in_map_nat : forall {n n' : nat}, natR n n' -> map_nat n = n' :=
 
 Definition R_in_mapK_nat : forall {n n' : nat} (nR : natR n n'),
   map_in_R_nat (R_in_map_nat nR) = nR.
-Proof. Admitted.
+Proof. 
+by move=> n n'; case: _ / => //= {}n {}n' nR; apply: natR_irrelevant.
+Qed.
 
 Definition Param_nat_sym {n n' : nat} : natR n n' -> natR n' n.
 Proof.
@@ -54,11 +76,7 @@ Defined.
 
 Definition Param_nat_sym_inv {n n' : nat} :
   forall (nR : natR n n'), Param_nat_sym (Param_nat_sym nR) = nR.
-Proof.
-  intro nR. induction nR; simpl.
-  - reflexivity.
-  - rewrite IHnR. reflexivity.
-Defined.
+Proof. by elim => //= {}n {}n' nR ->. Defined.
 
 Definition natR_sym : forall (n n' : nat), sym_rel natR n n' <->> natR n n'.
 Proof.

theories/Param_option.v

@@ -115,9 +115,9 @@ Definition option_R_in_map :
       | @noneR _ _ _ => idpath
       end.
 
-Definition option_R_in_mapK :
-  forall (A A' : Type) (AR : Param40.Rel A A')
-         (oa : option A) (oa' : option A') (oaR : optionR A A' AR oa oa'),
+Definition option_R_in_mapK (A A' : Type) (AR : Param40.Rel A A')
+         (oa : option A) (oa' : option A') (oaR : optionR A A' AR oa oa') :
     option_map_in_R A A' AR oa oa' (option_R_in_map A A' AR oa oa' oaR) = oaR.
 Proof.
-Admitted.
+by case: oaR => [a a' aR|]//=; elim/(ind_map AR): _; rewrite transport1.
+Qed.

theories/Param_paths.v

@@ -80,12 +80,10 @@ Definition paths_R_in_mapK@{i}
     paths_map_in_R@{i} A A' AR x x' xR y y' yR e e'
         (paths_R_in_map@{i} A A' AR x x' xR y y' yR e e' u) = u.
 Proof.
-  intros e e' r.
-  destruct r.
-  simpl.
-  elim (R_in_mapK AR x x' xR).
-  simpl.
-Admitted.
+move=> e e' [] //=.
+set X := (X in transport _ X _).
+have -> // : X = 1%path by exact: Prop_irrelevance.
+Qed.
 
 Definition Map0_paths
   A A' (AR : Param00.Rel A A') (x : A) (x' : A') (xR : AR x x')(y : A) (y' : A') (yR : AR y y') :

theories/Param_prod.v

@@ -92,7 +92,9 @@ Definition prod_R_in_mapK
     forall p p' (r : prodR AR BR p p'),
       prod_map_in_R A A' AR B B' BR p p' (prod_R_in_map A A' AR B B' BR p p' r) = r.
 Proof.
-Admitted.
+intros p p' []; rewrite /prod_R_in_map/=.
+by elim/(ind_map AR): _; elim/(ind_map BR): _.
+Qed.
 
 Definition Map0_prod A A' (AR : Param00.Rel A A') B B' (BR : Param00.Rel B B') :
   Map0.Has (prodR AR BR).

theories/Param_sigma.v

@@ -49,9 +49,8 @@ Definition sig_R_in_map
       sigR A A' AR P P' PR s s' -> sig_map A A' AR P P' PR s = s'.
 Proof.
   move=> [x Px] [u Py]; elim=> a a' aR p p' pR.
-  elim (R_in_map _ _ _ pR).
-  elim (R_in_mapK _ _ _ aR).
-  by case: _ / (R_in_map AR _ _ aR).
+  elim: (R_in_map _ _ _ pR) => {pR}.
+  by elim/(ind_map AR): _ aR / _.
 Defined.
 
 Definition sig_R_in_mapK
@@ -60,5 +59,7 @@ Definition sig_R_in_mapK
     forall (s : {x : A & P x}) (s' : {x' : A' & P' x'}),
       (sig_map_in_R A A' AR P P' PR s s') o (sig_R_in_map A A' AR P P' PR s s') == idmap.
 Proof.
-
-Admitted.
+move=> _ _ [a a' aR p p' pR] //=.
+elim/(ind_map (PR a a' aR)): _.
+by elim/(ind_mapP AR): _.
+Qed.