proposition: Lemma test_extensionality_1 : forall A1 (P Q : A1->Prop), (forall x1, P x1 <-> Q x1) -> P = Q.
proof: Proof. Proof using. intros. applys extensionality. hnf. Abort. Lemma test_extensionality_2 : forall A1 (A2: A1->Type) (P Q : forall (x1:A1) (x2:A2 x1), Prop), (forall x1 x2, P x1 x2 <-> Q x1 x2) -> P = Q. intros. applys extensionality. hnf. Abort. Section FuncExtDepTest. Variables (A1 : Type). Variables (A2 : forall (x1 : A1), Type). Variables (A3 : forall (x1 : A1) (x2 : A2 x1), Type). Variables (A4 : forall (x1 : A1) (x2 : A2 x1) (x3 : A3 x2), Type). Lemma test_fun_ext_3 : forall (f g : forall (x1:A1) (x2:A2 x1) (x3:A3 x2), A4 x3), (forall x1 x2 x3, f x1 x2 x3 = g x1 x2 x3) -> f = g. Proof using. intros. applys extensionality. hnf. Abort. End FuncExtDepTest. Lemma prop_ext_1_test : forall (P Q : Prop), (P <-> Q) -> P = Q. Proof using. intros. applys extensionality. simpl extensionality_hyp. Abort. Lemma absurds_demo : forall (P Q : Prop), P /\ (~ P) /\ (Q \/ ~ P). Proof using. intros. splits. { absurds ;=> H. admit. } { absurds ;=> H. admit. } { absurds ;=> (H1&H2). admit. } Abort. Module SubtermIndDemos. Import LibLogic LibList. Inductive tree : Type := | leaf : nat -> tree | node : list tree -> tree. Fixpoint tree_incr' (t:tree) := match t with | leaf n => leaf (S n) | node ts => node ((fix aux ts := match ts with | nil => nil | t::ts' => tree_incr' t :: aux ts' end) ts) end. Fixpoint tree_incr (t:tree) := match t with | leaf n => leaf (S n) | node ts => node (List.map tree_incr ts) end. Fixpoint tree_map (f:nat->nat) (t:tree) := match t with | leaf n => leaf (f n) | node ts => node (List.map (tree_map f) ts) end. Fixpoint tree_sum (t:tree) := match t with | leaf n => n | node ts => List.fold_left (fun acc t => acc + tree_sum t) ts 0 end. Section Tree_induct. Variables (P : tree -> Prop) (Q : list tree -> Prop) (P1 : forall n, P (leaf n)) (P2 : forall ts, Q ts -> P (node ts)) (Q1 : Q nil) (Q2 : forall t ts, P t -> Q ts -> Q (t::ts)). Fixpoint tree_induct_gen (t : tree) : P t := match t as x return P x with | leaf n => P1 n | node ts => P2 ((fix tree_list_induct (ts:list tree) : Q ts := match ts as x return Q x with | nil => Q1 | t::ts' => Q2 (tree_induct_gen t) (tree_list_induct ts') end) ts) end. End Tree_induct. Lemma tree_map_pred_succ_1 : forall t, tree_map pred (tree_map S t) = t. Proof using. intros. pattern t. match goal with |- ?F _ => sets P: F end. eapply tree_induct_gen with (Q := Forall P); subst P; simpl; intros. fequals. fequals. induction ts; simpl. fequals. inverts H. fequals~. constructors. constructors~. Qed.
imports: TLC(LibTactics) TLC(LibLogic LibEqual LibList LibRelation LibWf LibList LibLN)