[Coq-Club] [Agda] Re: [HoTT] newbie questions about homotopy
theory & advantage of UF/Coq
Matthieu Sozeau
matthieu.sozeau at gmail.com
Thu Jan 9 01:02:11 CET 2014
On 9 janv. 2014, at 00:41, Vladimir Voevodsky <vladimir at ias.edu> wrote:
>
> On Jan 8, 2014, at 6:39 PM, Matthieu Sozeau <matthieu.sozeau at gmail.com> wrote:
>
>> Well, take the transitive closure of p <_le le_succ n m p.
>> — Matthieu
>
> What is "p <_le le_succ n m p." ?
I guess that was a bit short indeed :) Here are the details. I’m using
packing with sigmas as it’s simpler to define the transitive closure
once and for all for homogeneous relations, there might be a more clever
way avoiding this:
I’m using Coq’s le in Prop, so I can’t prove wellfoundedness (this would
contradict the proof-irrelevance principle that Coq enforces). But with
everything in Set the proof would go through.
<<
Require Import Relation_Definitions.
Require Import Relation_Operators.
Require Import Transitive_Closure.
Scheme le_dep := Induction for le Sort Prop.
(* That's <_le *)
Inductive le_le : forall {n m n' m' : nat}, le n m -> le n' m' -> Prop :=
le_le_S : forall n m (p : le n m), le_le p (le_S _ _ p).
Definition relation A := A -> A -> Prop.
Definition le_hom : relation {n : nat & { m : nat & le n m }} :=
fun x y =>
let 'existT n (existT m p) := x in
let 'existT n' (existT m' p') := y in
le_le p p'.
Definition le_rel : relation {n : nat & { m : nat & le n m }} :=
clos_trans _ le_hom.
Require Import Program.
Goal forall x, Acc le_rel x.
Proof.
intros x. apply Acc_clos_trans.
destruct x as [n [m p]].
simpl. induction p using le_dep. constructor.
intros [n' [m' p']]. simpl.
intros. (* inversion H does not close this branch as we are in Prop and le_n can't be
discriminated from le_S *) admit.
constructor.
intros [n' [m' p']]. simpl.
intros.
(* inversion H fails again as we are in Prop, but we should now that
n = n', m = m' and p = p' and apply the induction hypothesis *)
admit.
Qed.
>>
Now you can (virtually, if you redo this in Set) make a “mathematical" induction
on derivations of [le], you just need to pack/curry the derivation with its indices
and apply the well-founded induction principle using the above proof.
— Matthieu
More information about the Agda
mailing list